Add a Makefile

4 files changed, 41 insertions, 13 deletions

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..bb42417
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,25 @@
+COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
+COQINCLUDES := -Q . predaware \
+               -R ../vericert/src vericert \
+               $(foreach d, $(COMPCERTRECDIRS), -R ../vericert/lib/CompCert/$(d) compcert.$(d)) \
+               -R ../vericert/lib/CompCert/flocq Flocq \
+               -R ../vericert/lib/CompCert/MenhirLib MenhirLib
+
+COQMAKE := $(COQBIN)coq_makefile
+
+VS := Main.v
+
+all: Makefile.coq _CoqProject
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq _CoqProject: force
+	@echo "COQMAKE Makefile.coq"
+	$(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq
+	echo "$(COQINCLUDES)" >_CoqProject
+
+force:
+
+clean:
+	git clean -dfx
+
+.PHONY: force all clean
diff --git a/_CoqProject b/_CoqProject
index 2255ae0..872ea42 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,11 +1 @@
--R ../vericert/src vericert
--R ../vericert/lib/CompCert/lib compcert.lib
--R ../vericert/lib/CompCert/common compcert.common
--R ../vericert/lib/CompCert/verilog compcert.verilog
--R ../vericert/lib/CompCert/backend compcert.backend
--R ../vericert/lib/CompCert/cfrontend compcert.cfrontend
--R ../vericert/lib/CompCert/driver compcert.driver
--R ../vericert/lib/CompCert/cparser compcert.cparser
--R ../vericert/lib/CompCert/flocq Flocq
--R ../vericert/lib/CompCert/MenhirLib MenhirLib
--Q . symb
+-Q . predaware -R ../vericert/src vericert  -R ../vericert/lib/CompCert/lib compcert.lib  -R ../vericert/lib/CompCert/common compcert.common  -R ../vericert/lib/CompCert/verilog compcert.verilog  -R ../vericert/lib/CompCert/backend compcert.backend  -R ../vericert/lib/CompCert/cfrontend compcert.cfrontend  -R ../vericert/lib/CompCert/driver compcert.driver  -R ../vericert/lib/CompCert/cparser compcert.cparser -R ../vericert/lib/CompCert/flocq Flocq -R ../vericert/lib/CompCert/MenhirLib MenhirLib
diff --git a/env.mkiv b/env.mkiv
index 1d74493..ee8619f 100644
--- a/env.mkiv
+++ b/env.mkiv
@@ -87,4 +87,10 @@
 
 \setupvimtyping[OrgBlkSrcCoq][margin=5mm]
 
+\setupregister[OrgConcept][
+  style={\bfa\tt},
+  color=darkcyan,
+  textstyle=tt,
+]
+
 \stopenvironment
diff --git a/main.org b/main.org
index 46cfc37..17194ef 100644
--- a/main.org
+++ b/main.org
@@ -4,6 +4,7 @@
 #+context_header_extra: \environment env
 #+options: syntax:vim toc:nil
 #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v
+#+auto_tangle: t
 
 One main optimisation in compilers targeting parallel architectures is /instruction scheduling/,
 where instructions are placed into time-slots statically so that these can be executed in parallel.
@@ -90,8 +91,8 @@ with expression_list : Type :=
 The interesting thing to note about this abstract expression type is that it is weakly typed,
 meaning predicates are not any different to standard expressions.  The correctness is therefore
 governed by how the expressions are generated, and to what resource they are assigned to in the
-final expression tree.  We will also need some kind of equality check for these expressions, so we
-can assume that we can implement a decidable check like the following:
+final expression tree.[fn:2] We will also need some kind of equality check for these expressions, so
+we can assume that we can implement a decidable check like the following:
 
 #+begin_src coq
 Axiom expression_dec:
@@ -122,6 +123,8 @@ Definition predicated A := NE.non_empty (pred_op * A).
 Definition pred_expr := predicated expression.
 #+end_src
 
+We can then also speak about equivalence between two predicates by
+
 #+begin_src coq
 Definition apred : Type := expression.
 Definition apred_op := @Predicate.pred_op apred.
@@ -240,5 +243,9 @@ End R_indexed.
 
 * Footnotes
 
+[fn:2] We can see that predicates are actually not needed in the semantics of any other
+expressions.  It might therefore be better to create a separate ~predicate_expression~ which will
+only set predicates based on a condition.
+
 [fn:1] This post uses noweb syntax to specify pieces of code defined elsewhere, and will link to
 those pieces of code directly.