.gitlab-ci.yml

@@ -135,7 +135,7 @@ spell-check:
   stage: build
   image: bbbrandenburg/aspell-ci
   script:
-    - scripts/flag-typos-in-comments.sh `find .  -iname '*.v'`
+    - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './doc/*'`
 
 # mathcomp-dev with stable Coq
 #coq-8.15:
@@ -153,6 +153,24 @@ spell-check:
 #  # it's ok to fail with an unreleased version of ssreflect and Coq
 #  allow_failure: true
 
+tutorial:
+  extends:
+   - .not_in_wip_branches
+  stage: build
+  image: bbbrandenburg/alectryon-ci:latest
+  script:
+    - eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
+    - opam update -y
+    - opam install -y -v -j ${NJOBS} --deps-only coq-prosa
+    - ./create_makefile.sh --without-refinements
+    - make -j ${NJOBS} tutorial
+    - mv html html-tutorial
+  artifacts:
+    name: "prosa-tutorial-$CI_COMMIT_REF_NAME"
+    paths:
+      - "html-tutorial/"
+    expire_in: 1 week
+
 proof-state:
   extends:
    - .not_in_wip_branches  

behavior/arrival_sequence.v

@@ -47,7 +47,7 @@ Section ValidArrivalSequence.
 
   (** Assume that job arrival times are known. *)
   Context {Job: JobType}.
-  Context `{JobArrival Job}.
+  Context {ja : JobArrival Job}.
 
   (** Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
@@ -76,7 +76,7 @@ Section ArrivalTimeProperties.
 
   (** Assume that job arrival times are known. *)
   Context {Job : JobType}.
-  Context `{JobArrival Job}.
+  Context {ja : JobArrival Job}.
 
   (** Let j be any job. *)
   Variable j : Job.
@@ -103,7 +103,7 @@ Section ArrivalSequencePrefix.
 
   (** Assume that job arrival times are known. *)
   Context {Job : JobType}.
-  Context `{JobArrival Job}.
+  Context {ja : JobArrival Job}.
 
   (** Consider any job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.

behavior/service.v

@@ -35,9 +35,9 @@ Section Service.
 
   (** In the following, consider jobs that have a cost, a deadline, and an
       arbitrary arrival time. *)
-  Context `{JobCost Job}.
-  Context `{JobDeadline Job}.
-  Context `{JobArrival Job}.
+  Context {jc : JobCost Job}.
+  Context {jd : JobDeadline Job}.
+  Context {ja : JobArrival Job}.
 
   (** We say that job [j] has completed by time [t] if it received all required
       service in the interval from [0] until (but not including) [t]. *)

create_makefile.sh

@@ -32,7 +32,7 @@ echo "${CoqProjectContent}" >> _CoqProject
 FIND_OPTS+=( -print )
 
 # Compile all relevant *.v files
-coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" | scripts/module-toc-order.py ) -o Makefile
+coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" | grep -v "doc/tutorial.v" | scripts/module-toc-order.py ) -o Makefile
 
 # Patch HTML target to switch out color, and 
 # so that it parses comments and has links to ssreflect.

scripts/Makefile.alectryon

@@ -4,3 +4,13 @@ html-alectryon/%.html: $(VOFILES)
 	$(HIDE)scripts/alectryon.sh $(patsubst %,%.v,$(subst html-alectryon/prosa/,,$(subst .,/,$(@:.html=))))
 
 alectryon: $(ALECTRYONFILES)
+
+tutorial: $(VOFILES) doc/tutorial.v
+	$(SHOW)'Compiling the tutorial with alectryon: doc/tutorial.v -> html/tutorial.html'
+	$(HIDE)mkdir -p html
+	$(HIDE)alectryon  -R . prosa --frontend coq+rst --backend webpage --output-directory "html" doc/tutorial.v 
+
+tutorial-pdf: $(VOFILES) doc/tutorial.v
+	$(SHOW)'Compiling the tutorial with alectryon: doc/tutorial.v -> doc/tutorial.pdf'
+	$(HIDE)alectryon  -R . prosa --frontend coq+rst --backend latex --output-directory "doc" doc/tutorial.v
+	$(HIDE)cd doc && pdflatex tutorial.tex

scripts/flag-typos-in-comments.sh

@@ -10,7 +10,7 @@ do
 
 	#Here, sed is used to remove verbatim text (enclosed in <<>>)
 	for WORD in $(scripts/extract-comments.py "$SRC" \
-		| sed 's/<<.*>>//g' \
+		| sed -e 's/<<.*>>//g' -e 's/`.*`//g' \
 		| aspell --add-extra-dicts=$KNOWN_EXCEPTIONS -l en  list \
 		| sort \
 		| uniq)

scripts/wordlist.pws

@@ -94,3 +94,13 @@ RTSS
 customizable
 uniprocessor's
 modularity
+ANR
+DFG
+MPI
+SWS
+INRIA
+Verimag
+ONERA
+OPAM
+Alectryon
+priori