initial compiling isl

hferee · Jan 16, 2024 · 65377cd · 65377cd
1 parent 83d36cc
commit 65377cd
Show file tree

Hide file tree

Showing 12 changed files with 6 additions and 100 deletions.
diff --git a/Makefile b/Makefile
@@ -1,21 +1,14 @@
 EXTRA_DIR:= doc-config
 COQDOCFLAGS:= \
-  --external 'http://ssr2.msr-inria.inria.fr/doc/ssreflect-1.5/' Ssreflect \
-  --external 'http://ssr2.msr-inria.inria.fr/doc/mathcomp-1.5/' MathComp \
   --toc --toc-depth 2 --html --interpolate \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
 export COQDOCFLAGS
 
 _: makefile.coq
 
-makefile.coq: _CoqProject
-	coq_makefile $(shell cat _CoqProject) _build/default/theories/iSL/*.v > $@ 2> /dev/null
-
-all: duneall
-
-duneall:
-	dune build --display short
+makefile.coq:
+	coq_makefile -f _CoqProject -o $@
 
 doc: makefile.coq
 	rm -fr html
@@ -26,14 +19,7 @@ doc: makefile.coq
 -include makefile.coq
 
 clean::
-	rm makefile.coq
-	dune clean
-	rm -f theories/.*.aux theories/*.glob theories/*.vo theories/*.glob
-
-demo: _build/default/bin/propquant.exe
-	_build/default/bin/propquant.exe $()
-
-release:
-	tar -zcvf release.tar.gz Makefile theories/*.v bin/ extraction _CoqProject  dune dune-project theories/dune README.md
+	rm makefile.coq makefile.coq.conf
+	rm -f theories/*/.*.aux theories/*/*.glob theories/*/*.vo theories/*/*.glob
 
 .PHONY: _
diff --git a/_CoqProject b/_CoqProject
@@ -1 +1,2 @@
--R _build/default/theories/iSL ISL
+-R theories/iSL ISL
+theories/iSL
diff --git a/dune b/dune
diff --git a/dune-project b/dune-project
diff --git a/theories/dune b/theories/dune
diff --git a/theories/Environments.v → theories/iSL/Environments.v b/theories/Environments.v → theories/iSL/Environments.v
diff --git a/theories/Formulas.v → theories/iSL/Formulas.v b/theories/Formulas.v → theories/iSL/Formulas.v
diff --git a/theories/Order.v → theories/iSL/Order.v b/theories/Order.v → theories/iSL/Order.v
diff --git a/theories/PropQuantifiers.v → theories/iSL/PropQuantifiers.v b/theories/PropQuantifiers.v → theories/iSL/PropQuantifiers.v
diff --git a/theories/SequentProps.v → theories/iSL/SequentProps.v b/theories/SequentProps.v → theories/iSL/SequentProps.v
diff --git a/theories/Sequents.v → theories/iSL/Sequents.v b/theories/Sequents.v → theories/iSL/Sequents.v
diff --git a/uiml.opam b/uiml.opam