[draft] Preliminary support for building with Dune

.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}))))

cparser/dune

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

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-project

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

extraction/dune.disabled

@@ -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/extraction.v

@@ -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

tools/dune

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

x86/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/extractionMachdep.v

@@ -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 *)