summaryrefslogtreecommitdiffstats
path: root/site
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-12 10:26:48 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-12 10:56:47 +0200
commitb85b9bc80bdb9b068ccfaffdfc975b8b0ba3a5de (patch)
treeff66f39ca7cfadbf997a04f242ea0abba35b4811 /site
parenta38a43028d05096369aa7bcec827bb6c08e3af8e (diff)
Various fixes here and there
Diffstat (limited to 'site')
-rw-r--r--site/cleopatra.org6
-rw-r--r--site/cleopatra/coq.org5
-rw-r--r--site/cleopatra/soupault.org3
-rw-r--r--site/cleopatra/theme.org11
-rw-r--r--site/index.org6
-rw-r--r--site/news/index.html10
-rw-r--r--site/posts/MiniHTTPServer.v193
7 files changed, 120 insertions, 114 deletions
diff --git a/site/cleopatra.org b/site/cleopatra.org
index 0f640bc..7060b66 100644
--- a/site/cleopatra.org
+++ b/site/cleopatra.org
@@ -1,5 +1,5 @@
#+BEGIN_EXPORT html
-A Series on Generating this Static Website
+<h1>A Series on Generating this Static Website</h1>
#+END_EXPORT
The generation of this website is far from being trivial, and requires the
@@ -36,12 +36,12 @@ written as literate programs.
<article class="index">
#+END_EXPORT
+- [[./cleopatra/theme.org][Theming with SASS ~(TODO)~]] ::
+
- [[file:cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]] ::
- [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]] ::
-- [[./cleopatra/theme.org][Theming with SASS ~(TODO)~]] ::
-
- [[./cleopatra/soupault.org][Processing HTML with ~soupault~]] ::
~soupault~ is a HTML processor, and it can be used as a static website
generator. We leverage *~soupault~* to provide a unified look and feel to a
diff --git a/site/cleopatra/coq.org b/site/cleopatra/coq.org
index a657fcf..51b0ecb 100644
--- a/site/cleopatra/coq.org
+++ b/site/cleopatra/coq.org
@@ -41,6 +41,11 @@ COQDOCARG := --no-index --charset utf8 --short \
div.code
white-space: nowrap
+.coq-text-block
+ @include patchy-centered
+ padding-top: 1rem
+ padding-bottom: 1rem
+
.doc
@include padding-centered
margin-top : 1em
diff --git a/site/cleopatra/soupault.org b/site/cleopatra/soupault.org
index dd90daf..04aec1f 100644
--- a/site/cleopatra/soupault.org
+++ b/site/cleopatra/soupault.org
@@ -125,6 +125,7 @@ contains a node matching a given ~selector~ (in the case of this document,
widget = "toc"
selector = "#generate-toc"
action = "replace_element"
+valid_html = true
min_level = 2
numbered_list = true
#+END_SRC
@@ -492,7 +493,7 @@ use to collect our initial history is
#+NAME: git-log
#+BEGIN_SRC bash :noweb no-export
-_git log --follow --pretty=format:'<<pretty-format>>' "${file}"
+_git log -n4 --follow --pretty=format:'<<pretty-format>>' "${file}"
#+END_SRC
To manipulate JSON, we rely on three operators (yet to be defined):
diff --git a/site/cleopatra/theme.org b/site/cleopatra/theme.org
index 3bba6b7..c7b0145 100644
--- a/site/cleopatra/theme.org
+++ b/site/cleopatra/theme.org
@@ -12,7 +12,7 @@ theme-build : ${SASS}
soupault-build : theme-build
-ARTIFACTS += ${CSS} ${SASS}
+ARTIFACTS += ${CSS}
#+END_SRC
* Main HTML Template
@@ -121,7 +121,7 @@ $remark-fg: #4d575e
$sans-serif : sans-serif
-$document-width : 33rem
+$document-width : 38rem
a
color : #557de8
@@ -145,7 +145,7 @@ a:visited
margin-right : 1rem
@mixin text-font
- font-family : et-book, serif
+ font-family : serif
@mixin code-font($size : .9rem)
font-family: 'Fira Code', monospace
@@ -223,8 +223,9 @@ body#default
h1
text-align: center
- h1, h2, h3, h4, h5, h6
- font-family : $sans-serif
+ h2, h3, h4, h5, h6
+ font-style: italic
+
code, tt
font-size: 100%
diff --git a/site/index.org b/site/index.org
index 749877b..df5fad2 100644
--- a/site/index.org
+++ b/site/index.org
@@ -80,9 +80,9 @@ process.
you are guaranteed that the code you read is the code that has been used to
generate the HTML page you read it from.
- 1. [[./cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]]
- 2. [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]]
- 3. [[./cleopatra/theme.org][Theming with SASS ~(TODO)~]]
+ 1. [[./cleopatra/theme.org][Theming with SASS ~(TODO)~]]
+ 2. [[./cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]]
+ 3. [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]]
4. [[./cleopatra/soupault.org][Processing HTML with ~soupault~]]
- [[./posts/Thanks.html][Thanks!]] ::
diff --git a/site/news/index.html b/site/news/index.html
index 5191f75..1bbb731 100644
--- a/site/news/index.html
+++ b/site/news/index.html
@@ -4,11 +4,21 @@
<ul>
<li>
+ On <strong>April 17, 2020</strong>, my first contribution to
+ Dune <a href="https://github.com/ocaml/dune/pull/3384">has been merged
+ to <code>master</code></a>.
+ </li>
+ <li>
On <strong>April 2, 2020</strong>, I started using the rewriting of
<a href="https://cleopatra.soap.coffee"><strong><code>cleopatra</code></strong></a>
to build this website.
</li>
<li>
+ On <strong>April 1, 2020</strong>, my first contribution ever to
+ Coq <a href="https://github.com/coq/coq/pull/10592">has been merged
+ to <code>master</code></a>.
+ </li>
+ <li>
On <strong>February 23, 2020</strong>,
<strong><code>cleopatra</code></strong> has been completely
bootstrapped, in that it generates itself!
diff --git a/site/posts/MiniHTTPServer.v b/site/posts/MiniHTTPServer.v
index 075d5c8..dda5841 100644
--- a/site/posts/MiniHTTPServer.v
+++ b/site/posts/MiniHTTPServer.v
@@ -17,7 +17,7 @@
The [FreeSpec.Core] module reexports the key component provided by
FreeSpec. *)
-From FreeSpec Require Import Core.
+From FreeSpec.Core Require Import All.
(** ** Implementation *)
@@ -67,12 +67,12 @@ Axiom socket_descriptor : Type.
Inductive TCP : interface :=
(** - [NewTCPSocket] is a primitive to create a socket. It takes as an argument
- the address of the socket (of the form <<[url]:[port]>>) of type [bytes]
+ the address of the socket (of the form <<[url]:[port]>>) of type [bytestring]
(a type provided by the <<coq-prelude>> project with a convenient string
notation). It returns a [socket_descriptor] to interact with the newly
created socket. *)
-| NewTCPSocket (addr : bytes)
+| NewTCPSocket (addr : bytestring)
: TCP socket_descriptor
(** - [ListenIncomingConnection] changes the mode of a given socket identified
@@ -93,11 +93,11 @@ Inductive TCP : interface :=
(** - [ReadSocket] and [WriteSocket] allows to receive data from and send data
to the socket, that is interacting with the client. They also use the
- [bytes] type *)
+ [bytestring] type *)
| ReadSocket (socket : socket_descriptor)
- : TCP bytes
-| WriteSocket (socket : socket_descriptor) (msg : bytes)
+ : TCP bytestring
+| WriteSocket (socket : socket_descriptor) (msg : bytestring)
: TCP unit
(** - Finally, [CloseTCPSocket] interrupts an existing connection by closing the
@@ -134,7 +134,7 @@ Generalizable All Variables.
automatically, thanks to the [MetaCoq] project. *)
Definition new_tcp_socket `{Provide ix TCP}
- (addr : bytes)
+ (addr : bytestring)
: impure ix socket_descriptor :=
request (NewTCPSocket addr).
@@ -150,11 +150,11 @@ Definition accept_connection `{Provide ix TCP}
Definition read_socket `{Provide ix TCP}
(socket : socket_descriptor)
- : impure ix bytes :=
+ : impure ix bytestring :=
request (ReadSocket socket).
Definition write_socket `{Provide ix TCP}
- (socket : socket_descriptor) (msg : bytes)
+ (socket : socket_descriptor) (msg : bytestring)
: impure ix unit :=
request (WriteSocket socket msg).
@@ -172,13 +172,13 @@ Definition close_socket `{Provide ix TCP}
Axiom file_descriptor : Type.
Inductive FILESYSTEM : interface :=
-| Open (path : bytes) : FILESYSTEM file_descriptor
-| FileExists (file : bytes) : FILESYSTEM bool
-| Read (file : file_descriptor) : FILESYSTEM bytes
+| Open (path : bytestring) : FILESYSTEM file_descriptor
+| FileExists (file : bytestring) : FILESYSTEM bool
+| Read (file : file_descriptor) : FILESYSTEM bytestring
| Close (file : file_descriptor) : FILESYSTEM unit.
Definition open `{Provide ix FILESYSTEM}
- (path : bytes)
+ (path : bytestring)
: impure ix file_descriptor :=
request (Open path).
@@ -188,29 +188,26 @@ Definition close `{Provide ix FILESYSTEM}
request (Close fd).
Definition file_exists `{Provide ix FILESYSTEM}
- (path : bytes)
+ (path : bytestring)
: impure ix bool :=
request (FileExists path).
Definition read `{Provide ix FILESYSTEM}
(fd : file_descriptor)
- : impure ix bytes :=
+ : impure ix bytestring :=
request (Read fd).
(** **** The [CONSOLE] Interface *)
-(** Finally, FreeSpec already provides a few generic interfaces for FreeSpec
- users, including a [CONSOLE] interface:
-
-<<
Inductive CONSOLE : interface :=
-| Scan : CONSOLE bytes
-| Echo : bytes -> CONSOLE unit.
->>
+| Scan : CONSOLE bytestring
+| Echo : bytestring -> CONSOLE unit.
- It is defined in the [FreeSpec.Stdlib.Console] module. *)
+Definition scan `{Provide ix CONSOLE} : impure ix bytestring :=
+ request Scan.
-From FreeSpec.Stdlib Require Import Console.
+Definition echo `{Provide ix CONSOLE} (msg : bytestring) : impure ix unit :=
+ request (Echo msg).
(** *** Implementing a HTTP Server *)
@@ -221,7 +218,7 @@ From FreeSpec.Stdlib Require Import Console.
To that end, we rely on the <<coq-prelude>> package, and therefore import
it. *)
-From Prelude Require Import All Bytes.
+From Base Require Import Prelude.
(** **** A Word on Non-Termination *)
@@ -242,7 +239,7 @@ Fixpoint repeatM `{Monad m} {a}
: m unit :=
match n with
| O => pure tt
- | S n => do p >>= fun _ => repeatM n p end
+ | S n => p >>= fun _ => repeatM n p
end.
(** **** A Generic TCP Server *)
@@ -252,23 +249,21 @@ Fixpoint repeatM `{Monad m} {a}
response message for each request message received from a client. *)
Definition tcp_server `{Provide ix TCP}
- (n : nat) (handler : bytes -> impure ix bytes)
+ (n : nat) (handler : bytestring -> impure ix bytestring)
: impure ix unit :=
- do let* server := new_tcp_socket "127.0.0.1:8088" in
- listen_incoming_connection server;
+ let* server := new_tcp_socket "127.0.0.1:8088" in
+ listen_incoming_connection server;;
- repeatM n do
- let* client := accept_connection server in
+ repeatM n (
+ let* client := accept_connection server in
- let* req := read_socket client in
- let* res := handler req in
- write_socket client res;
+ let* req := read_socket client in
+ let* res := handler req in
+ write_socket client res;;
- close_socket client
- end;
+ close_socket client);;
- close_socket server
- end.
+ close_socket server.
(** **** A HTTP Handler *)
@@ -283,16 +278,15 @@ Definition tcp_server `{Provide ix TCP}
FreeSpec provides [Provide2], [Provide3], [Provide4], and [Provide5] to make
the type more readable. *)
-Definition read_content `{Provide2 ix FILESYSTEM CONSOLE}
- (path : bytes)
- : impure ix bytes :=
- do echo (" reading <" ++ path ++ ">... ");
- let* fd := open path in
- let* c := read fd in
- close fd;
- echo ("done.\n");
- pure c
- end.
+Timeout 2 Definition read_content `{Provide2 ix FILESYSTEM CONSOLE}
+ (path : bytestring)
+ : impure ix bytestring :=
+ echo (" reading <" ++ path ++ ">... ");;
+ let* fd := open path in
+ let* c := read fd in
+ close fd;;
+ echo "done.\n";;
+ pure c.
(** Using this utility function, we can define the handler itself.
@@ -307,7 +301,7 @@ From MiniHTTPServer Require Import URI HTTP.
- [http_req] encodes the supported HTTP requests (currently, only GET
requests are supported).
- - [http_request] a parsing function of the form [bytes -> error_stack +
+ - [http_request] a parsing function of the form [bytestring -> error_stack +
http_req]
- [http_res] encodes the HTTP responses used by MiniHTTPServer (in our
case, 200, 401, and 404)
@@ -318,35 +312,32 @@ Definition request_handler `{Provide2 ix FILESYSTEM CONSOLE}
: impure ix response :=
match req with
| Get uri =>
- do let path := uri_to_path (sandbox base uri) in
- let* isf := file_exists path in
- if (isf : bool)
- then make_response success_OK <$> read_content path
- else do
- echo (" resource <" ++ path ++"> not found\n");
- pure (make_response client_error_NotFound
- "Resource not found.")
- end
- end
+ let path := uri_to_path (sandbox base uri) in
+ let* isf := file_exists path in
+ if (isf : bool)
+ then make_response success_OK <$> read_content path
+ else (
+ echo (" resource <" ++ path ++"> not found\n");;
+ pure (make_response client_error_NotFound
+ "Resource not found."))
end.
Definition http_handler `{Provide2 ix FILESYSTEM CONSOLE}
- (base : list directory_id) (req : bytes)
- : impure ix bytes :=
- do echo "new request received\n";
- echo (" request size is "
- ++ Int.bytes_of_int (Bytes.length req)
- ++ "\n");
-
- let* res :=
- match http_request req with
- | inr req => request_handler base (fst req)
- | _ => pure (make_response client_error_BadRequest
- "Bad request")
- end in
-
- pure (response_to_string res)
- end.
+ (base : list directory_id) (req : bytestring)
+ : impure ix bytestring :=
+ echo "new request received\n";;
+ echo (" request size is "
+ ++ bytestring_of_int (Bytestring.length req)
+ ++ "\n");;
+
+ let* res :=
+ match http_request req with
+ | inr req => request_handler base (fst req)
+ | _ => pure (make_response client_error_BadRequest
+ "Bad request")
+ end in
+
+ pure (response_to_string res).
(** Since [read_content] uses the [CONSOLE] interface in addition to
[FILESYSTEM], our [http_handler] type exposes this explicitely. However,
@@ -362,9 +353,8 @@ Definition http_server
`{Provide3 ix FILESYSTEM TCP CONSOLE}
(n : nat)
: impure ix unit :=
- do echo "hello, MiniHTTPServer!\n";
- tcp_server n (http_handler [Dirname "tmp"])
- end.
+ echo "hello, MiniHTTPServer!\n";;
+ tcp_server n (http_handler [Dirname "tmp"]).
(** ** Certifying *)
@@ -498,9 +488,9 @@ Inductive fd_set_caller_obligation (ω : fd_set)
(** We do not restrict the use of [Open] or [FileExists] *)
-| fd_set_open_caller (p : bytes)
+| fd_set_open_caller (p : bytestring)
: fd_set_caller_obligation ω file_descriptor (Open p)
-| fd_set_is_file_caller (p : bytes)
+| fd_set_is_file_caller (p : bytestring)
: fd_set_caller_obligation ω bool (FileExists p)
(** In order for [Read] and [Close] to be used correctly, their
@@ -508,7 +498,7 @@ Inductive fd_set_caller_obligation (ω : fd_set)
| fd_set_read_caller (fd : file_descriptor)
(is_member : member ω fd)
- : fd_set_caller_obligation ω bytes (Read fd)
+ : fd_set_caller_obligation ω bytestring (Read fd)
| fd_set_close_caller (fd : file_descriptor)
(is_member : member ω fd)
: fd_set_caller_obligation ω unit (Close fd).
@@ -536,7 +526,7 @@ Inductive fd_set_callee_obligation (ω : fd_set)
(** The [file_descriptor] returned by the [Open] primitive shall not be a member
of the witness state. *)
-| fd_set_open_callee (p : bytes) (fd : file_descriptor)
+| fd_set_open_callee (p : bytestring) (fd : file_descriptor)
(is_absent : absent ω fd)
: fd_set_callee_obligation ω file_descriptor (Open p) fd
@@ -546,11 +536,11 @@ Inductive fd_set_callee_obligation (ω : fd_set)
another contract, which is totally fine with FreeSpec since we can compose
them together. *)
-| fd_set_read_callee (fd : file_descriptor) (s : bytes)
- : fd_set_callee_obligation ω bytes (Read fd) s
+| fd_set_read_callee (fd : file_descriptor) (s : bytestring)
+ : fd_set_callee_obligation ω bytestring (Read fd) s
| fd_set_close_callee (fd : file_descriptor) (t : unit)
: fd_set_callee_obligation ω unit (Close fd) t
-| fd_set_is_file_callee (p : bytes) (b : bool)
+| fd_set_is_file_callee (p : bytestring) (b : bool)
: fd_set_callee_obligation ω bool (FileExists p) b.
Hint Constructors fd_set_callee_obligation : minihttp.
@@ -638,7 +628,7 @@ Lemma fd_set_preserving_http_server
Lemma fd_set_respectful_read_content
`{StrictProvide2 ix FILESYSTEM CONSOLE}
- (ω : fd_set) (path : bytes)
+ (ω : fd_set) (path : bytestring)
: respectful_impure fd_set_contract ω (read_content path).
(** FreeSpec provides the [prove_impure] tactics to automate as much as possible
@@ -651,7 +641,7 @@ Lemma fd_set_respectful_read_content
<<
ω : fd_set
- path : bytes
+ path : bytestring
x : unit
H4 : gen_callee_obligation fd_set_contract ω
(inj_p (Echo (" reading <" ++ path ++ ">... "))) x
@@ -660,7 +650,7 @@ Lemma fd_set_respectful_read_content
(gen_witness_update fd_set_contract ω
(inj_p (Echo (" reading <" ++ path ++ ">... "))) x)
(inj_p (Open path)) x0
- x1 : bytes
+ x1 : bytestring
H6 : gen_callee_obligation fd_set_contract
(gen_witness_update fd_set_contract
(gen_witness_update fd_set_contract ω
@@ -693,7 +683,7 @@ subgoal 1 is:
fd_set_caller_obligation ω file_descriptor (Open path)
subgoal 2 is:
- fd_set_caller_obligation (add_fd ω x0) bytes (Read x0)
+ fd_set_caller_obligation (add_fd ω x0) bytestring (Read x0)
subgoal 3 is:
fd_set_caller_obligation (add_fd ω x0) unit (Close x0)
@@ -714,7 +704,7 @@ Hint Resolve fd_set_respectful_read_content : minihttp.
Lemma fd_set_preserving_read_content
`{StrictProvide2 ix FILESYSTEM CONSOLE}
- (path : bytes)
+ (path : bytestring)
: fd_set_preserving (read_content path).
(** Similarly to [prove_impure], FreeSpec provides a tactic to exploit
@@ -734,9 +724,9 @@ Lemma fd_set_preserving_read_content
This produces the following goal:
<<
- path : bytes
+ path : bytestring
ω : fd_set
- x : bytes
+ x : bytestring
x0 : unit
o_callee : gen_callee_obligation fd_set_contract ω
(inj_p (Echo (" reading <" ++ path ++ ">... "))) x0
@@ -812,7 +802,7 @@ Qed.
Lemma fd_set_respectful_file_exists
`{Provide ix FILESYSTEM}
- (ω : fd_set) (path : bytes)
+ (ω : fd_set) (path : bytestring)
: respectful_impure fd_set_contract ω (file_exists path).
Proof.
@@ -822,7 +812,7 @@ Qed.
Hint Resolve fd_set_respectful_file_exists : minihttp.
Lemma fd_set_preserving_file_exists
- `{Provide ix FILESYSTEM} (path : bytes)
+ `{Provide ix FILESYSTEM} (path : bytestring)
: fd_set_preserving (file_exists path).
Proof.
@@ -849,7 +839,7 @@ Qed.
Lemma fd_set_respectful_http_handler
`{StrictProvide2 ix FILESYSTEM CONSOLE}
- (base : list directory_id) (req : bytes)
+ (base : list directory_id) (req : bytestring)
(ω : fd_set)
: respectful_impure fd_set_contract ω (http_handler base req).
@@ -881,7 +871,7 @@ Hint Resolve fd_set_respectful_http_handler : minihttp.
Lemma fd_set_preserving_http_handler
`{StrictProvide2 ix FILESYSTEM CONSOLE}
- (base : list directory_id) (req : bytes)
+ (base : list directory_id) (req : bytestring)
: fd_set_preserving (http_handler base req).
Proof.
@@ -956,17 +946,16 @@ Qed.
Lemma fd_set_preserving_tcp_server_repeat_routine
`{Provide ix TCP, MayProvide ix FILESYSTEM, Distinguish ix TCP FILESYSTEM}
(server : socket_descriptor)
- (handler : bytes -> impure ix bytes)
- (preserve : forall (req : bytes), fd_set_preserving (handler req))
- : fd_set_preserving (do
+ (handler : bytestring -> impure ix bytestring)
+ (preserve : forall (req : bytestring), fd_set_preserving (handler req))
+ : fd_set_preserving (
let* client := accept_connection server in
let* req := read_socket client in
let* res := handler req in
- write_socket client res;
+ write_socket client res;;
- close_socket client
- end).
+ close_socket client).
Proof.
intros ω ω' b run fd.