make coqdoc to work

.github/dependabot.yml

@@ -0,0 +1,9 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"

.github/workflows/ci_build.yaml

@@ -35,7 +35,16 @@ jobs:
 
       - name: repo checkout
         uses: actions/checkout@v3
-
+
+      - name: Initialise variables
+        run: |
+          # Only deploy if the build follows from pushing to master
+          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
+             echo "DOC_DEPLOY=true" >> $GITHUB_ENV
+          else
+             echo "DOC_DEPLOY=false" >> $GITHUB_ENV
+          fi
+          
       - name: container registry log in
         uses: docker/login-action@v3
         with:
@@ -56,19 +65,21 @@ jobs:
               sudo chown -R coq:coq .
             endGroup
           script: |
-            startGroup "Build Coq lib"
-              cd theories/
-              make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
+            startGroup "Build binary"
+              if [[ "$DOC" ]]; then
+                make coqdoc
+              else
+                make
+              fi
             endGroup
           after_script: |
-            startGroup "Build binary"
-              cd ..
-              make
+            startGroup "after"
             endGroup
           export: "OPAMJOBS OPAMYES"
         env:
           OPAMJOBS: ${{ steps.cpu-cores.outputs.count }}
           OPAMYES: "true"
+          DOC: ${{ env.DOC_DEPLOY }}
 
       - name: permissions revert
         # to avoid a warning at cleanup time

Makefile

@@ -4,6 +4,9 @@ all:
 	@$(MAKE) -C theories
 	@dune build
 
+coqdoc: all
+	@${MAKE} coqdoc -C theories
+
 clean:
 	@$(MAKE) clean -C theories
 	@dune clean

theories/Core/Semantic/Domain.v

@@ -50,7 +50,7 @@ Module Domain_Notations.
   Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope.
   Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope.
-  Notation "x" := x (in custom domain at level 0, x global) : mcltt_scope.
+  Notation "x" := x (in custom domain at level 0, x ident) : mcltt_scope.
   Notation "'λ' ρ M" := (d_fn ρ M) (in custom domain at level 0, ρ custom domain at level 30, M custom exp at level 30) : mcltt_scope.
   Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope.
   Notation "'ℕ'" := d_nat (in custom domain) : mcltt_scope.

theories/Core/Syntactic/Syntax.v

@@ -125,7 +125,7 @@ Module Syntax_Notations.
   Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope.
   Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : mcltt_scope.
-  Notation "x" := x (in custom exp at level 0, x global) : mcltt_scope.
+  Notation "x" := x (in custom exp at level 0, x ident) : mcltt_scope.
   Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : mcltt_scope.
   Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : mcltt_scope.
   Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mcltt_scope.
@@ -149,7 +149,7 @@ Module Syntax_Notations.
   Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope.
   Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : mcltt_scope.
-  Notation "x" := x (in custom nf at level 0, x global) : mcltt_scope.
+  Notation "x" := x (in custom nf at level 0, x ident) : mcltt_scope.
   Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : mcltt_scope.
   Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mcltt_scope.
   Notation "'ℕ'" := nf_nat (in custom nf) : mcltt_scope.

theories/Makefile

@@ -21,21 +21,13 @@ MENHIR := menhir
 
 COQMAKEFILE := CoqMakefile.mk
 COQPROJECTFILE := _CoqProject
-PARSERBASE := parser.ml
-POSTPARSERBASE := type_checker.ml
-PARSERFILE := ../driver/$(PARSERBASE)
-POSTPARSERFILE := ../driver/$(POSTPARSERBASE)
-FRONTENDDIR := Frontend
-PARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/ParserExtraction.v
-PARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(PARSERBASE)
-POSTPARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/PostParserExtraction.v
-POSTPARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(POSTPARSERBASE)
+PARSERBASE := Parser.ml
+POSTPARSERBASE := Entrypoint.ml
+PARSERFILE := ../driver/extracted/$(PARSERBASE)
+POSTPARSERFILE := ../driver/extracted/$(POSTPARSERBASE)
 COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
 COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
 
-COQDOCJS_DIR:=../assets/
-include Makefile.doc
-
 .PHONY: all
 all: $(COQMAKEFILE)
 	@+$(MAKE) -j "${NPROCS}" -f "$(COQMAKEFILE)" all
@@ -61,14 +53,13 @@ update_CoqProject: clean
 .PHONY: force
 force: ;
 
-# html: $(COQMAKEFILE)
-# 	@+$(MAKE) -j "${NPROCS}" -f "$(COQMAKEFILE)" html
-# 	@cp -rf "${EXTRA_DIR}"/* html/
-
 $(COQMAKEFILE): $(COQPROJECTFILE)
 	$(COQBIN)coq_makefile -f "$?" -o "$@"
 
 $(COQPROJECTFILE): ;
 
 %: $(COQMAKEFILE) force
 	@+$(MAKE) -f "$(COQMAKEFILE)" "$@"
+
+COQDOCJS_DIR:=../assets/
+include Makefile.doc