Skip to content

Commit ca98bdb

Browse files
ejgallegoejgallego
committed
[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.
1 parent d357b5c commit ca98bdb

File tree

11 files changed

+288
-23
lines changed

11 files changed

+288
-23
lines changed

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,3 +82,6 @@
8282
.nia.cache
8383
.nra.cache
8484
.csdp.cache
85+
86+
_build
87+
.merlin

‎backend/dune‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
(rule
2+
(targets SplitLong.v)
3+
(action
4+
(with-stdout-to %{targets}
5+
(run ndfun %{dep:SplitLong.vp}))))
6+
7+
(rule
8+
(targets SelectDiv.v)
9+
(action
10+
(with-stdout-to %{targets}
11+
(run ndfun %{dep:SelectDiv.vp}))))

‎compcert.opam‎

Whitespace-only changes.

‎cparser/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(rule
2+
(targets Parser.v)
3+
(action
4+
(run menhir --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check %{dep:Parser.vy})))

‎dune‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
(coq.theory
2+
(name compcert)
3+
(package compcert)
4+
(modules :standard \ common.Subtyping x86.extractionMachdep)
5+
(flags
6+
-w -unused-pattern-matching-variable
7+
-w -deprecated-ident-entry
8+
-w -deprecated-hint-rewrite-without-locality
9+
-w -undeclared-scope))
10+
11+
(include_subdirs qualified)
12+
13+
(dirs :standard \ arm powerpc riscV aarch64 x86_64 flocq)
14+
15+
(env
16+
(_ (binaries tools/ndfun.exe)))
17+

‎dune-project‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
(lang dune 3.3)
2+
(using coq 0.4)
3+
(using menhir 2.1)
4+
5+
(name compcert)

‎extraction/dune.disabled‎

Lines changed: 198 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,198 @@
1+
(coq.extraction
2+
(prelude extraction)
3+
(extracted_modules
4+
Allocation
5+
Alphabet
6+
Archi
7+
Ascii
8+
Asmgen
9+
Asm
10+
AST
11+
Automaton
12+
Binary
13+
BinInt
14+
BinNat
15+
BinNums
16+
BinPosDef
17+
BinPos
18+
Bits
19+
BoolEqual
20+
Bool
21+
Bounds
22+
Bracket
23+
Builtins0
24+
Builtins1
25+
Builtins
26+
Cabs
27+
Cexec
28+
CleanupLabels
29+
Clight
30+
Cminorgen
31+
Cminor
32+
CminorSel
33+
Cminortyping
34+
CombineOp
35+
Compare_dec
36+
Compiler
37+
Compopts
38+
Constprop
39+
ConstpropOp
40+
Conventions1
41+
Conventions
42+
Cop
43+
Coqlib
44+
CSEdomain
45+
CSE
46+
Csem
47+
Csharpminor
48+
Cshmgen
49+
Csyntax
50+
Ctypes
51+
Ctyping
52+
Datatypes
53+
Deadcode
54+
Debugvar
55+
DecidableClass
56+
Decidableplus
57+
DecidableType
58+
Determinism
59+
Digits
60+
Equalities
61+
EquivDec
62+
Errors
63+
Events
64+
Floats
65+
FLT
66+
FMapAVL
67+
FMapList
68+
FSetAVL
69+
FSetAVLplus
70+
FSetInterface
71+
Globalenvs
72+
Grammar
73+
Heaps
74+
IEEE754_extra
75+
Initializers
76+
Inlining
77+
Int0
78+
Integers
79+
Interpreter_complete
80+
Interpreter_correct
81+
Interpreter
82+
IntvSets
83+
Iteration
84+
Kildall
85+
Lattice
86+
Linearize
87+
Linear
88+
Lineartyping
89+
List0
90+
Liveness
91+
Locations
92+
LTL
93+
Mach
94+
Machregs
95+
Main
96+
Maps
97+
Memdata
98+
Memory
99+
Memtype
100+
Mergesort
101+
MSetAVL
102+
MSetInterface
103+
Nat
104+
NeedDomain
105+
NeedOp
106+
Op
107+
Ordered
108+
OrderedType
109+
OrdersAlt
110+
OrdersFacts
111+
Orders
112+
OrdersTac
113+
Parser
114+
PeanoNat
115+
Postorder
116+
Registers
117+
Renumber
118+
Ring
119+
Round
120+
RTLgen
121+
RTL
122+
RTLtyping
123+
SelectDiv
124+
Selection
125+
SelectLong
126+
SelectOp
127+
SimplExpr
128+
SimplLocals
129+
Specif
130+
SplitLong
131+
Stacking
132+
Stacklayout
133+
String0
134+
Switch
135+
Tailcall
136+
Tunneling
137+
UnionFind
138+
Unityping
139+
Unusedglob
140+
Validator_complete
141+
Validator_safe
142+
ValueAnalysis
143+
ValueAOp
144+
ValueDomain
145+
Values
146+
ZArith_dec
147+
Zaux
148+
Zbits
149+
Zbool
150+
Znumtheory
151+
Zpower)
152+
(theories compcert))
153+
154+
(include_subdirs no)
155+
156+
(library
157+
(name compcert)
158+
(wrapped false)
159+
(modules_without_implementation C debugTypes dwarfTypes)
160+
(modules :standard \ Driver GCC)
161+
(flags -w -32)
162+
(libraries menhirLib))
163+
164+
(copy_files %{project_root}/backend/*.{ml,mli})
165+
(copy_files %{project_root}/common/*.{ml,mli})
166+
(copy_files %{project_root}/lib/*.{ml,mli,mll})
167+
(copy_files %{project_root}/driver/*.{ml,mli})
168+
(copy_files %{project_root}/cfrontend/*.{ml,mli})
169+
(copy_files %{project_root}/cparser/*.{ml,mli})
170+
(copy_files %{project_root}/cparser/pre_parser.mly)
171+
(copy_files %{project_root}/cparser/handcrafted.messages)
172+
(copy_files %{project_root}/cparser/Lexer.mll)
173+
(copy_files %{project_root}/debug/*.{ml,mli})
174+
(copy_files %{project_root}/x86/*.{ml,mli})
175+
176+
(ocamllex Lexer Tokenize Readconfig Responsefile)
177+
(menhir
178+
(modules pre_parser)
179+
(flags --table -v --no-stdlib -la 1))
180+
181+
(executable
182+
(name Driver)
183+
(public_name ccomp)
184+
(modules Driver)
185+
(libraries str unix compcert))
186+
187+
(rule
188+
(targets pre_parser_messages.ml)
189+
(action
190+
(with-stdout-to %{targets}
191+
(run menhir --table pre_parser.mly -v --no-stdlib -la 1 -v -la 2 --compile-errors %{dep:handcrafted.messages}))))
192+
193+
(rule
194+
(targets version.ml)
195+
(action
196+
(with-stdout-to %{targets}
197+
(bash "cat ../VERSION | sed -e 's|\\(.*\\)=\\(.*\\)|let \\1 = \\\"\\2\\\"|g'"))))
198+

‎extraction/extraction.v‎

Lines changed: 22 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -14,27 +14,28 @@
1414
(* *)
1515
(* *********************************************************************)
1616

17-
Require Coqlib.
18-
Require Wfsimpl.
19-
Require DecidableClass Decidableplus.
20-
Require AST.
21-
Require Iteration.
22-
Require Floats.
23-
Require SelectLong.
24-
Require Selection.
25-
Require RTLgen.
26-
Require Inlining.
27-
Require ValueDomain.
28-
Require Tailcall.
29-
Require Allocation.
30-
Require Bounds.
31-
Require Ctypes.
32-
Require Csyntax.
33-
Require Ctyping.
34-
Require Clight.
35-
Require Compiler.
36-
Require Parser.
37-
Require Initializers.
17+
From compcert Require Coqlib.
18+
From compcert Require Wfsimpl.
19+
From Coq Require DecidableClass.
20+
From compcert Require Decidableplus.
21+
From compcert Require AST.
22+
From compcert Require Iteration.
23+
From compcert Require Floats.
24+
From compcert Require SelectLong.
25+
From compcert Require Selection.
26+
From compcert Require RTLgen.
27+
From compcert Require Inlining.
28+
From compcert Require ValueDomain.
29+
From compcert Require Tailcall.
30+
From compcert Require Allocation.
31+
From compcert Require Bounds.
32+
From compcert Require Ctypes.
33+
From compcert Require Csyntax.
34+
From compcert Require Ctyping.
35+
From compcert Require Clight.
36+
From compcert Require Compiler.
37+
From compcert Require Parser.
38+
From compcert Require Initializers.
3839

3940
(* Standard lib *)
4041
Require Import ExtrOcamlBasic.
@@ -149,8 +150,6 @@ Set Extraction AccessOpaque.
149150

150151
(* Go! *)
151152

152-
Cd "extraction".
153-
154153
Separate Extraction
155154
Compiler.transf_c_program Compiler.transf_cminor_program
156155
Cexec.do_initial_state Cexec.do_step Cexec.at_final_state

‎tools/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(executable
2+
(name ndfun)
3+
(flags :standard -w -27)
4+
(modules ndfun)
5+
(libraries str))
6+
7+
(include_subdirs no)

‎x86/dune‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
(rule
2+
(targets SelectOp.v)
3+
(action
4+
(with-stdout-to %{targets}
5+
(run ndfun SelectOp.vp))))
6+
7+
(rule
8+
(targets ConstpropOp.v)
9+
(action
10+
(with-stdout-to %{targets}
11+
(run ndfun ConstpropOp.vp))))
12+
13+
(rule
14+
(targets SelectLong.v)
15+
(action
16+
(with-stdout-to %{targets}
17+
(run ndfun SelectLong.vp))))
18+
19+

0 commit comments

Comments
 (0)