Compiler: move CIL/ into src/

.gitlab-ci.yml

@@ -55,7 +55,7 @@ coq-program:
   artifacts:
     paths:
     - proofs/
-    - compiler/CIL/
+    - compiler/src/CIL/
 
 coq-proof:
   stage: prove
@@ -143,7 +143,7 @@ opam-compiler:
     nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
     'eval $(opam env) &&
      make -C compiler -j$NIX_BUILD_CORES &&
-     (cd compiler && mkdir -p bin && cp _build/default/jasminc.exe bin/jasminc)'
+     (cd compiler && mkdir -p bin && cp _build/default/entry/jasminc.exe bin/jasminc)'
   artifacts:
     paths:
     - compiler/bin/jasminc

MANIFEST

@@ -19,11 +19,10 @@ compiler/entry/jasminc.ml
 compiler/src/LICENSE.puf
 compiler/scripts/runtest
 compiler/Makefile
-compiler/dune
+find:compiler:dune
 compiler/dune-project
-compiler/src/dune
 compiler/jasmin.opam
-compiler/CIL/.keep
+compiler/src/CIL/.keep
 compiler/config/tests.config
 
 # EasyCrypt library

compiler/MANIFEST

@@ -4,20 +4,18 @@ README.md
 
 default.nix
 Makefile
-dune
 dune-project
-src/dune
 jasmin.opam
 
-find:CIL:*.ml
-find:CIL:*.mli
+find:.:dune
+
 find:entry:*.ml
 find:src:*.ml
 find:src:*.mli
 find:src:*.mll
 find:src:*.mly
 
 src/LICENSE.puf
-CIL/LICENSE.coq
-CIL/LICENSE.coqword
-CIL/LICENSE.mathcomp
+src/CIL/LICENSE.coq
+src/CIL/LICENSE.coqword
+src/CIL/LICENSE.mathcomp

compiler/Makefile

@@ -35,10 +35,10 @@ build: native
 
 define do-build
 	$(RM) jasminc jazz2tex
-	dune build jasminc.$(1)
-	dune build jazz2tex.$(1)
-	ln -sf "_build/default/jasminc.$(1)" jasminc
-	ln -sf "_build/default/jazz2tex.$(1)" jazz2tex
+	dune build entry/jasminc.$(1)
+	dune build entry/jazz2tex.$(1)
+	ln -sf "_build/default/entry/jasminc.$(1)" jasminc
+	ln -sf "_build/default/entry/jazz2tex.$(1)" jazz2tex
 endef
 
 byte:
@@ -48,10 +48,10 @@ native:
 	$(call do-build,exe)
 
 CIL:
-	rm -f CIL/*.ml CIL/*.mli ../proofs/extraction.vo
+	rm -f src/CIL/*.ml src/CIL/*.mli ../proofs/extraction.vo
 	$(MAKE) -C ../proofs extraction
-	cp ../proofs/lang/ocaml/*.ml  CIL/
-	cp ../proofs/lang/ocaml/*.mli CIL/
+	cp ../proofs/lang/ocaml/*.ml  src/CIL/
+	cp ../proofs/lang/ocaml/*.mli src/CIL/
 
 check: build
 	$(CHECK) --report=report.log $(CHECKCATS)

compiler/README.md

@@ -11,9 +11,9 @@ The files `src/puf.ml` and `src/puf.mli` are distributed under the terms of the
 GNU Library General Public License version 2.1, with the special exception on
 linking described in file [`src/LICENSE.puf`](src/LICENSE.puf).
 
-The contents of the `CIL` directory are extracted from Coq files from several sources:
+The contents of the `src/CIL` directory are extracted from Coq files from several sources:
 
- -  the Coq standard library (LGPL 2.1 only, see [`CIL/LICENSE.coq`](CIL/LICENSE.coq))
- -  the Mathematical Components library (CēCILL-B, see [`CIL/LICENSE.mathcomp`](CIL/LICENSE.mathcomp))
- -  the coqword library (MIT, see [`CIL/LICENSE.coqword`](CIL/LICENSE.coqword))
+ -  the Coq standard library (LGPL 2.1 only, see [`src/CIL/LICENSE.coq`](src/CIL/LICENSE.coq))
+ -  the Mathematical Components library (CēCILL-B, see [`src/CIL/LICENSE.mathcomp`](src/CIL/LICENSE.mathcomp))
+ -  the coqword library (MIT, see [`src/CIL/LICENSE.coqword`](src/CIL/LICENSE.coqword))
  -  the Jasmin coq source files (MIT, the [same license](LICENSE) as the rest of the compiler).

compiler/default.nix

@@ -11,7 +11,7 @@ stdenv.mkDerivation {
     mkdir -p $out/bin
     for p in jasminc jazz2tex
     do
-      cp _build/default/$p.exe $out/bin/$p
+      cp _build/default/entry/$p.exe $out/bin/$p
     done
   '';
 }

compiler/dune

@@ -4,9 +4,7 @@
   (release
     (flags (:standard -w +Z+Y+28-23+32+33+34-58@8))))
 
-(dirs src CIL entry)
-(include_subdirs unqualified)
-
+(subdir entry
 (executable
  (public_name jasminc)
  (name jasminc)
@@ -22,10 +20,4 @@
  (flags -rectypes)
  (modes byte exe)
  (libraries cmdliner jasmin))
-
-(library
- (name jasmin)
- (public_name jasmin.jasmin)
- (modules :standard \ jasminc jazz2tex)
- (flags -rectypes)
- (libraries batteries zarith menhirLib yojson apron.octMPQ apron.ppl apron.boxMPQ))
+)

compiler/jasmin.opam

@@ -13,8 +13,8 @@ build: [
 ]
 install: [
   mkdir -p "%{prefix}%/bin"
-  cp "_build/default/jasminc.exe" "%{prefix}%/bin/jasminc"
-  cp "_build/default/jazz2tex.exe" "%{prefix}%/bin/jazz2tex"
+  cp "_build/default/entry/jasminc.exe" "%{prefix}%/bin/jasminc"
+  cp "_build/default/entry/jazz2tex.exe" "%{prefix}%/bin/jazz2tex"
 ]
 depends: [
   "ocaml" { >= "4.10" & build }

compiler/src/dune

@@ -1,6 +1,14 @@
+(include_subdirs unqualified)
+
 (ocamllex
  (modules lexer))
 
 (menhir
  (flags "--table" "--explain")
  (modules parser))
+
+(library
+ (name jasmin)
+ (public_name jasmin.jasmin)
+ (flags -rectypes)
+ (libraries batteries zarith menhirLib yojson apron.octMPQ apron.ppl apron.boxMPQ))