[Build] WIP: project dunification

Dockerfile

@@ -9,6 +9,7 @@ RUN opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 RUN opam install -y ott zarith
 COPY . .
 RUN opam pin add -y --no-action coq-albert .
+RUN opam pin remove dune
 RUN opam depext -y coq-albert
 RUN opam install -y -j ${NJOBS} --deps-only .
 RUN opam install -y -j ${NJOBS} --with-test .

Makefile

@@ -62,7 +62,8 @@ COQ_FILES_LIST = \
 	progress.v
 COQ_FILES=$(COQ_FILES_LIST:%=$(COQ_DIR)/%)
 
-all: $(COQ_DIR)/Makefile $(COQ_FILES) all-vo compiler
+all: $(COQ_DIR)/Makefile $(COQ_FILES) # all-vo compiler
+	dune build
 
 test: compiler
 	make -C examples
@@ -158,7 +159,7 @@ LEXER=$(PARSER_DIR)/lexer.mll
 AST=$(PARSER_DIR)/ast.ml
 
 
-$(PARSER) $(LEXER): $(OTT_FILES)
+$(PARSER) $(LEXER) $(AST): $(OTT_FILES)
 	cd parser;	$(OTT) -merge true $(^:%.ott=-i ../%.ott) -o $(AST_FILE) -o $(PARSER_FILE) -o $(LEXER_FILE) \
 	-tex_suppress_ntr g
 # Rewrite the parser to fit the extracted code
@@ -179,7 +180,7 @@ extraction/lexer.ml: $(LEXER)
 clean::
 	rm -f $(OTT_TEX) proposal_final.pdf
 	cd $(TEX_DIR); rm -f  *.aux *.bbl *.blg *.log *.out *.pdf *.toc
-	cd $(COQ_DIR); rm -f *.vo *.glob albert.* Makefile Makefile.conf
+	cd $(COQ_DIR); rm -f *.vo *.glob albert.* Makefile Makefile.conf .*.aux
 	rm -f $(PARSER) $(LEXER) $(PARSER_PP) $(AST)
 	make -C extraction clean 
 	make -C examples clean 

coq-albert.opam

@@ -14,7 +14,7 @@ build: [
 ]
 install: [ make "install" ]
 depends: [
-  "dune"
+  "dune" {>= "2.5.0"}
   "ott"
   "menhir"
   "coq" {>= "8.8.2"}

coq/dune

+(coq.theory
+  (name Albert)
+  (modules (:standard \ operations))
+)
+
+(rule
+  (target albert.v)
+  ( deps
+    ../ott/header.ott
+    ../ott/base.ott
+    ../ott/fail.ott
+    ../ott/toplevel_definition.ott
+    ../ott/arith.ott
+    ../ott/unit.ott
+    ../ott/pair.ott
+    ../ott/drop.ott
+    ../ott/dup.ott
+    ../ott/pattern_matching.ott
+    ../ott/variant.ott
+    ../ott/option.ott
+    ../ott/or.ott
+    ../ott/bool.ott
+    ../ott/string.ott
+    ../ott/bytes.ott
+    ../ott/compare.ott
+    ../ott/list.ott
+    ../ott/map.ott
+    ../ott/crypto.ott
+    ../ott/operation.ott)
+    (action (chdir %{workspace_root}
+          (run %{bin:ott} -merge true -coq_expand_list_types false
+  -signal_parse_errors true -o %{target} %{deps}))))

dune-project

+(lang dune 2.5)
+(name coq-albert)
+(using coq 0.2)
+(using menhir 2.1)

extraction/dune

@@ -3,3 +3,69 @@
  (public_names albert_c)
  (flags (:standard -w -33-39-27))
 )
+
+(rule
+   (target lexer.ml)
+   (deps ../parser/lexer.mll)
+   (action (chdir %{workspace_root}
+          (run %{bin:ocamllex} -q -o %{target} %{deps}))))
+
+(menhir
+   (modules "../parser/parser" "../parser/menhir_lib")
+   (merge_into parser))
+
+(coq.extraction
+  (prelude extraction)
+  (theories Albert)
+  (extracted_modules albert
+                     All0
+                     All1
+                     All
+                     Ascii
+                     BinInt
+                     BinNat
+                     BinNums
+                     BinPosDef
+                     BinPos
+                     Bool
+                     Bvector
+                     Byte
+                     Char0
+                     Datatypes
+                     Date
+                     Decimal
+                     DecimalString
+                     Equalities
+                     error
+                     Fin
+                     int64
+                     label_lexico
+                     lexico_sort
+                     List0
+                     List
+                     location
+                     Logic
+                     LString
+                     Mergesort
+                     micheline_pp
+                     micheline_syntax
+                     michelson2micheline
+                     michocomp
+                     Moment
+                     Nat
+                     Orders
+                     PeanoNat
+                     Plus
+                     pretty_printers
+                     Specif
+                     String
+                     syntax_type
+                     tez
+                     Time
+                     typer
+                     untyped_syntax
+                     Util
+                     VectorDef
+                     Vector
+                     Zdigits
+                     ))