[draft] Preliminary support for building with Dune

Dear CompCert developers, this is a proof-of-concept highlighting a
full build of x86 using the Dune build system.

The PR is not meant to be merged yet, but as a demonstration and to
gather feedback. In particular, it has a few quirks that should be
solved soon Dune upstream:

- no proper configuration
- mixed Coq/ML dirs require a hack
- only works with Dune master

IMHO, I think it would make sense to eventually finish and merge this
PR, either as the main build system, or as secondary one, to be used
in Coq's Continous Integration system.

Dune support is very interesting for Coq developers as it allows for
composed, incremental builds with Coq itself; this means a large
speed-up in practice.

Author: ejgallego

.gitignore

@@ -82,3 +82,6 @@
 .nia.cache
 .nra.cache
 .csdp.cache
+
+_build
+.merlin

backend/dune

@@ -0,0 +1,11 @@
+(rule
+ (targets SplitLong.v)
+ (action
+  (with-stdout-to %{targets}
+   (run ndfun %{dep:SplitLong.vp}))))
+
+(rule
+ (targets SelectDiv.v)
+ (action
+  (with-stdout-to %{targets}
+   (run ndfun %{dep:SelectDiv.vp}))))

compcert.opam

@@ -0,0 +1,4 @@
+(rule
+ (targets Parser.v)
+ (action
+  (run menhir --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check %{dep:Parser.vy})))

cparser/dune

@@ -0,0 +1,17 @@
+(coq.theory
+ (name compcert)
+ (package compcert)
+ (modules :standard \ common.Subtyping x86.extractionMachdep extraction.extraction)
+ (flags
+   -w -unused-pattern-matching-variable
+   -w -deprecated-ident-entry
+   -w -deprecated-hint-rewrite-without-locality
+   -w -undeclared-scope))
+
+(include_subdirs qualified)
+
+(dirs :standard \ arm powerpc riscV aarch64 x86_64 flocq)
+
+(env
+ (_ (binaries tools/ndfun.exe)))
+

dune

@@ -0,0 +1,5 @@
+(lang dune 3.3)
+(using coq 0.4)
+(using menhir 2.1)
+
+(name compcert)

dune-project

@@ -0,0 +1,198 @@
+(coq.extraction
+ (prelude extraction)
+ (extracted_modules
+   Allocation
+   Alphabet
+   Archi
+   Ascii
+   Asmgen
+   Asm
+   AST
+   Automaton
+   Binary
+   BinInt
+   BinNat
+   BinNums
+   BinPosDef
+   BinPos
+   Bits
+   BoolEqual
+   Bool
+   Bounds
+   Bracket
+   Builtins0
+   Builtins1
+   Builtins
+   Cabs
+   Cexec
+   CleanupLabels
+   Clight
+   Cminorgen
+   Cminor
+   CminorSel
+   Cminortyping
+   CombineOp
+   Compare_dec
+   Compiler
+   Compopts
+   Constprop
+   ConstpropOp
+   Conventions1
+   Conventions
+   Cop
+   Coqlib
+   CSEdomain
+   CSE
+   Csem
+   Csharpminor
+   Cshmgen
+   Csyntax
+   Ctypes
+   Ctyping
+   Datatypes
+   Deadcode
+   Debugvar
+   DecidableClass
+   Decidableplus
+   DecidableType
+   Determinism
+   Digits
+   Equalities
+   EquivDec
+   Errors
+   Events
+   Floats
+   FLT
+   FMapAVL
+   FMapList
+   FSetAVL
+   FSetAVLplus
+   FSetInterface
+   Globalenvs
+   Grammar
+   Heaps
+   IEEE754_extra
+   Initializers
+   Inlining
+   Int0
+   Integers
+   Interpreter_complete
+   Interpreter_correct
+   Interpreter
+   IntvSets
+   Iteration
+   Kildall
+   Lattice
+   Linearize
+   Linear
+   Lineartyping
+   List0
+   Liveness
+   Locations
+   LTL
+   Mach
+   Machregs
+   Main
+   Maps
+   Memdata
+   Memory
+   Memtype
+   Mergesort
+   MSetAVL
+   MSetInterface
+   Nat
+   NeedDomain
+   NeedOp
+   Op
+   Ordered
+   OrderedType
+   OrdersAlt
+   OrdersFacts
+   Orders
+   OrdersTac
+   Parser
+   PeanoNat
+   Postorder
+   Registers
+   Renumber
+   Ring
+   Round
+   RTLgen
+   RTL
+   RTLtyping
+   SelectDiv
+   Selection
+   SelectLong
+   SelectOp
+   SimplExpr
+   SimplLocals
+   Specif
+   SplitLong
+   Stacking
+   Stacklayout
+   String0
+   Switch
+   Tailcall
+   Tunneling
+   UnionFind
+   Unityping
+   Unusedglob
+   Validator_complete
+   Validator_safe
+   ValueAnalysis
+   ValueAOp
+   ValueDomain
+   Values
+   ZArith_dec
+   Zaux
+   Zbits
+   Zbool
+   Znumtheory
+   Zpower)
+ (theories compcert))
+
+(include_subdirs no)
+
+(library
+ (name compcert)
+ (wrapped false)
+ (modules_without_implementation C debugTypes dwarfTypes)
+ (modules :standard \ Driver GCC)
+ (flags -w -32)
+ (libraries menhirLib))
+
+(copy_files %{project_root}/backend/*.{ml,mli})
+(copy_files %{project_root}/common/*.{ml,mli})
+(copy_files %{project_root}/lib/*.{ml,mli,mll})
+(copy_files %{project_root}/driver/*.{ml,mli})
+(copy_files %{project_root}/cfrontend/*.{ml,mli})
+(copy_files %{project_root}/cparser/*.{ml,mli})
+(copy_files %{project_root}/cparser/pre_parser.mly)
+(copy_files %{project_root}/cparser/handcrafted.messages)
+(copy_files %{project_root}/cparser/Lexer.mll)
+(copy_files %{project_root}/debug/*.{ml,mli})
+(copy_files %{project_root}/x86/*.{ml,mli})
+
+(ocamllex Lexer Tokenize Readconfig Responsefile)
+(menhir
+ (modules pre_parser)
+ (flags --table -v --no-stdlib -la 1))
+
+(executable
+ (name Driver)
+ (public_name ccomp)
+ (modules Driver)
+ (libraries str unix compcert))
+
+(rule
+ (targets pre_parser_messages.ml)
+ (action
+  (with-stdout-to %{targets}
+   (run menhir --table pre_parser.mly -v --no-stdlib -la 1 -v -la 2 --compile-errors %{dep:handcrafted.messages}))))
+
+(rule
+ (targets version.ml)
+ (action
+   (with-stdout-to %{targets}
+    (bash "cat ../VERSION | sed -e 's|\\(.*\\)=\\(.*\\)|let \\1 = \\\"\\2\\\"|g'"))))
+

extraction/dune.disabled

@@ -14,27 +14,28 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Coqlib.
-Require Wfsimpl.
-Require DecidableClass Decidableplus.
-Require AST.
-Require Iteration.
-Require Floats.
-Require SelectLong.
-Require Selection.
-Require RTLgen.
-Require Inlining.
-Require ValueDomain.
-Require Tailcall.
-Require Allocation.
-Require Bounds.
-Require Ctypes.
-Require Csyntax.
-Require Ctyping.
-Require Clight.
-Require Compiler.
-Require Parser.
-Require Initializers.
+From compcert Require Coqlib.
+From compcert Require Wfsimpl.
+From Coq Require DecidableClass.
+From compcert Require Decidableplus.
+From compcert Require AST.
+From compcert Require Iteration.
+From compcert Require Floats.
+From compcert Require SelectLong.
+From compcert Require Selection.
+From compcert Require RTLgen.
+From compcert Require Inlining.
+From compcert Require ValueDomain.
+From compcert Require Tailcall.
+From compcert Require Allocation.
+From compcert Require Bounds.
+From compcert Require Ctypes.
+From compcert Require Csyntax.
+From compcert Require Ctyping.
+From compcert Require Clight.
+From compcert Require Compiler.
+From compcert Require Parser.
+From compcert Require Initializers.
 
 (* Standard lib *)
 Require Import ExtrOcamlBasic.
@@ -149,8 +150,6 @@ Set Extraction AccessOpaque.
 
 (* Go! *)
 
-Cd "extraction".
-
 Separate Extraction
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state

extraction/extraction.v

@@ -0,0 +1,7 @@
+(executable
+ (name ndfun)
+ (flags :standard -w -27)
+ (modules ndfun)
+ (libraries str))
+
+(include_subdirs no)

tools/dune

@@ -0,0 +1,17 @@
+(rule
+ (targets SelectOp.v)
+ (action
+  (with-stdout-to %{targets}
+   (run ndfun %{dep:SelectOp.vp}))))
+
+(rule
+ (targets ConstpropOp.v)
+ (action
+  (with-stdout-to %{targets}
+   (run ndfun %{dep:ConstpropOp.vp}))))
+
+(rule
+ (targets SelectLong.v)
+ (action
+  (with-stdout-to %{targets}
+   (run ndfun %{dep:SelectLong.vp}))))

x86/dune

@@ -16,6 +16,8 @@
 
 (* Additional extraction directives specific to the x86-64 port *)
 
+(* This was in original dune PR *)
+(* From compcert Require SelectOp ConstpropOp. *)
 Require Archi SelectOp.
 
 (* Archi *)