From b85b9bc80bdb9b068ccfaffdfc975b8b0ba3a5de Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Sun, 12 Jul 2020 10:26:48 +0200 Subject: Various fixes here and there --- .gitignore | 2 +- site/cleopatra.org | 6 +- site/cleopatra/coq.org | 5 ++ site/cleopatra/soupault.org | 3 +- site/cleopatra/theme.org | 11 +-- site/index.org | 6 +- site/news/index.html | 10 +++ site/posts/MiniHTTPServer.v | 193 +++++++++++++++++++++----------------------- 8 files changed, 121 insertions(+), 115 deletions(-) diff --git a/.gitignore b/.gitignore index 6aac4b9..ffa58a7 100644 --- a/.gitignore +++ b/.gitignore @@ -31,6 +31,7 @@ build.log .*.aux *.glob .lia.cache +site/posts/AlgebraicDatatypes.html site/posts/StronglySpecifiedFunctionsProgram.html site/posts/MiniHTTPServer.html site/posts/ClightIntroduction.html @@ -51,5 +52,4 @@ site/posts/MonadTransformers.html site/posts/CleopatraV1.html build/ site/style/main.css -site/style/main.sass # end generated files 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 +

A Series on Generating this Static Website

#+END_EXPORT The generation of this website is far from being trivial, and requires the @@ -36,12 +36,12 @@ written as literate programs.
#+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:'<>' "${file}" +_git log -n4 --follow --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 @@ -3,11 +3,21 @@

Hobbyist Projects

    +
  • + On April 17, 2020, my first contribution to + Dune has been merged + to master. +
  • On April 2, 2020, I started using the rewriting of cleopatra to build this website.
    • +
  • + On April 1, 2020, my first contribution ever to + Coq has been merged + to master. +
  • On February 23, 2020, cleopatra has been completely 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 <> 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 <> 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. -- cgit v1.2.3