Output modern HOL4 syntax, fix up builds of HOL4 examples (#114)

* convert ottScript.sml to modern HOL4

* modernize ottLib and add Holmakefile with basic test

* output HOL4 Inductive syntax for trindemossen-1 and later

* output HOL4 Type abbrevation syntax for kananaskis-14 and later

* adjust HOL4 newlines to be similar to Coq output

* make HOL4 rule label names follow Coq naming conventions

* fix up hol-def and coq-def build of ocaml_light example

* simplify ocaml_light Makefile, fix some hol theories for trindemossen-1

* fix up test10st_metatheoryScript.sml for trindemossen-1

* fix up leroy-jfp96.ott to check in HOL4 trindemossen-1

* make ocaml_light basicScript.sml compile with trindemossen-1

* update documentation for trindemossen-1 related changes

.holpath

@@ -0,0 +1 @@
+OTTDIR

doc/top2.mng

@@ -888,7 +888,7 @@ e.g.~a usage of \verb+v'+ where \verb+v<::t+, an additional premise
 invoking the generated  subrule predicate for the non-free rule is added, e.g.~\verb+is_v v'+.
 For Coq and HOL, explicit quantifiers are introduced for all variables
 mentioned in the rule.
-For HOL, rules are tagged with their rule name (using \verb+clause_name+).
+For HOL, rules are labelled with their rule name and tagged using \verb+clause_name+.
 
 
 \subsection{Representation of binding}

examples/ocaml_light/.gitignore

@@ -6,6 +6,9 @@
 *.v.d
 *.aux
 .coqdeps.d
+.HOLMK
+.hollogs
+.holobjs
 caml_typedef.dvi
 caml_typedef.lem
 caml_typedef.log
@@ -17,6 +20,7 @@ caml_typedef.thy
 caml_typedef.toc
 caml_typedef.v
 caml_typedefScript.sml
+caml_typedefTheory.sig
 caml_typedef_reduction.ott
 caml_typedef_syntax.ott
 caml_typedef_typing.ott

examples/ocaml_light/Holmakefile

@@ -0,0 +1,4 @@
+INCLUDES = $(OTTDIR)/hol
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all

examples/ocaml_light/Makefile

@@ -25,7 +25,7 @@ ott: caml_typedef.tex caml_typedef.v caml_typedefScript.sml caml_typedef.thy
 ps: caml_typedef.ps
 pdf: caml_typedef.pdf
 coq-def: caml_typedef.vo
-hol-def: caml_typedefTheory.uo hol_caml
+hol-def: caml_typedefTheory.uo
 isa-def: caml_typedef.isa
 coq: coq-def
 hol: hol-def
@@ -35,23 +35,21 @@ hol-proof: hol/definitionsTheory.uo hol/defs_red_funTheory.uo
 install_doc: caml_typedef.pdf
 	cp caml_typedef.pdf doc/built_doc
 
+.PHONY: ott ps pdf coq-def hol-def isa-def coq hol isa hol-proof install_doc
+
 #### Directories ####
 ############ CHANGE topdir TO REFER TO YOUR TOP LEVEL OTT INSTALLATION ########
 topdir = ../..
 #/home/so294/scratch/ott_distro_0.10.13
 ott_coq_lib_dir = $(topdir)/coq
-ott_hol_lib_dir = $(topdir)/hol
 poly_lib = /Users/so294/polyml.5.1/lib
 
 #### Programs and their arguments ####
 COQC = coqc
-#COQ_INCLUDE = -I $(ott_coq_lib_dir)
-COQ_INCLUDE = -Q $(ott_coq_lib_dir) Ott
-COQ_FLAGS =
+COQ_FLAGS = -Q $(ott_coq_lib_dir) Ott
 DVIPS = dvips
 DVIPSFLAGS = -Ppdf -j0 -G0
 HOLMAKE = Holmake
-HOLMAKE_INCLUDE = -I $(ott_hol_lib_dir)
 HOLMAKE_FLAGS = --qof
 ISABELLE = isabelle
 ISABELLE_FLAGS = -q
@@ -153,39 +151,30 @@ caml_combinations.v: $(caml_combinations:=.v) ;
 	$(PS2PDF) $< $@
 
 #### Coq ####
-coq_libs = $(ott_coq_lib_dir)/ott_list
-coq-libs: $(coq_libs:=.vo)
-$(coq_libs:=.vo): %:
-	cd $(@D) && $(MAKE) $(@F)
-.SUFFIXES: .v .vo
-.v.vo:
-	$(COQC) $(COQ_INCLUDE) $(COQ_FLAGS) $<
+coq-lib:
+	cd $(ott_coq_lib_dir) && $(MAKE)
+.PHONY: coq-lib
+%.vo: %.v coq-lib
+	$(COQC) $(COQ_FLAGS) $<
 
 #### Hol ####
 dummy:
+.PHONY: dummy
 
 hol_caml.o: caml_typedefTheory.uo hol_caml.ML
 	hol.builder < hol_caml.ML
 
 hol_caml: hol_caml.o
 	cc -L$(poly_lib) -o hol_caml -lpolymain -lpolyml hol_caml.o
 
-hol_libs = $(topdir)/hol/ottLib $(topdir)/hol/ottTheory
-hol-libs: $(hol_libs:=.ui) $(hol_libs:=.uo)
-$(hol_libs:=.ui) $(hol_libs:=.uo): %:
-	cd $(@D) && $(MAKE) $(@F)
-%Theory.uo: %Script.sml hol-libs
-	$(HOLMAKE) $(HOLMAKE_INCLUDE) $(HOLMAKE_FLAGS) $@
-hol/Holmakefile: Makefile
-	rm -f hol/Holmakefile
-	echo INCLUDES = .. ../$(ott_hol_lib_dir) > hol/Holmakefile
-hol/testing/Holmakefile: Makefile
-	rm -f hol/testing/Holmakefile
-	echo INCLUDES = .. ../.. $(ott_hol_lib_dir) > hol/testing/Holmakefile
-hol/definitionsTheory.uo: caml_typedefTheory.uo hol/Holmakefile hol/testing/Holmakefile dummy hol-def
-	cd $(@D) && $(HOLMAKE) $(HOLMAKE_FLAGS) --poly ../hol_caml $(@F)
-hol/defs_red_funTheory.uo: caml_typedefTheory.uo hol/Holmakefile hol/testing/Holmakefile dummy hol-def
-	cd $(@D) && $(HOLMAKE) $(HOLMAKE_FLAGS) --poly ../hol_caml $(@F)
+caml_typedefTheory.uo: caml_typedefScript.sml
+	$(HOLMAKE) $(HOLMAKE_FLAGS) $@
+
+hol/definitionsTheory.uo: caml_typedefTheory.uo dummy
+	cd $(@D) && $(HOLMAKE) $(HOLMAKE_FLAGS) $(@F)
+
+hol/defs_red_funTheory.uo: caml_typedefTheory.uo dummy
+	cd $(@D) && $(HOLMAKE) $(HOLMAKE_FLAGS) $(@F)
 
 hol/ocamlpp/filter:
 	cd $(@D) && $(MAKE) $(@F)

examples/ocaml_light/hol/.gitignore

@@ -0,0 +1,4 @@
+.HOLMK
+.hollogs
+.holobjs
+*Theory.sig

examples/ocaml_light/hol/Holmakefile

@@ -0,0 +1,4 @@
+INCLUDES = $(OTTDIR)/hol $(OTTDIR)/examples/ocaml_light
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all