Merge branch 'master' of github.com:sacerdot/matita

sacerdot · Sep 26, 2023 · 1caef17 · 1caef17
2 parents 8fe832d + 71b993b
commit 1caef17
Show file tree

Hide file tree

Showing 67 changed files with 62 additions and 5 deletions.
diff --git a/components/binaries/Makefile b/components/binaries/Makefile
@@ -1,9 +1,9 @@
 H=@
 
-#CSC: saturate is broken after the huge refactoring of auto/paramodulation
-#CSC: by Andrea
-#BINARIES=extractor  table_creator  utilities saturate transcript
-#FG: my binaries
+#FG matex renders lamdba-terms to LaTeX
+#FG matitadep exports the dependencies of .ma files
+#FG probe returns statistics on compiled files
+#FG xoa generates matita files for n-ary logical operators/quantifiers
 BINARIES=matex matitadep probe xoa
 
 all: $(BINARIES:%=rec@all@%) 

diff --git a/components/broken_binaries/Makefile b/components/broken_binaries/Makefile
@@ -0,0 +1,18 @@
+H=@
+
+#CSC: saturate is broken after the huge refactoring of auto/paramodulation
+#CSC: by Andrea
+#CSC: the others have not been maintained for a while or they are now useless
+BINARIES=
+
+all: $(BINARIES:%=rec@all@%) 
+opt: $(BINARIES:%=rec@opt@%)
+depend: $(BINARIES:%=rec@depend@%)
+depend.opt: $(BINARIES:%[email protected]@%)
+install: $(BINARIES:%=rec@install@%)
+uninstall: $(BINARIES:%=rec@uninstall@%)
+clean: $(BINARIES:%=rec@clean@%) 
+
+rec@%:
+	$(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
+
diff --git a/components/broken_binaries/Makefile.common b/components/broken_binaries/Makefile.common
@@ -0,0 +1,25 @@
+H=@
+
+include ../../../Makefile.defs
+
+DIST=$(EXEC)---$(VERSION)
+DATE=$(shell date +%y%m%d)
+
+OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" 
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) 
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS)
+
+opt:
+	@echo "  OCAMLBUILD $(EXEC).native" 
+	$(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" $(EXEC).native 
+
+clean:
+	ocamlbuild -clean
+	rm -rf $(DIST) $(DIST).tgz
+
+dist:
+	mkdir -p $(DIST)/Sources
+	cp ReadMe $(DIST)
+	cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources
+	cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC)
+	tar -cvzf $(DIST).tgz $(DIST)
diff --git a/components/binaries/dump_db/dump.sh → components/broken_binaries/dump_db/dump.sh b/components/binaries/dump_db/dump.sh → components/broken_binaries/dump_db/dump.sh
diff --git a/components/binaries/matitaprover/CASC_2008 → ...ts/broken_binaries/matitaprover/CASC_2008 b/components/binaries/matitaprover/CASC_2008 → ...ts/broken_binaries/matitaprover/CASC_2008
diff --git a/components/binaries/matitaprover/FIXME → ...onents/broken_binaries/matitaprover/FIXME b/components/binaries/matitaprover/FIXME → ...onents/broken_binaries/matitaprover/FIXME
diff --git a/components/binaries/matitaprover/Makefile → ...nts/broken_binaries/matitaprover/Makefile b/components/binaries/matitaprover/Makefile → ...nts/broken_binaries/matitaprover/Makefile
diff --git a/...matitaprover/SystemDescriptionMatita.html → ...matitaprover/SystemDescriptionMatita.html b/...matitaprover/SystemDescriptionMatita.html → ...matitaprover/SystemDescriptionMatita.html
diff --git a/...ts/binaries/matitaprover/TreeLimitedRun.c → ...en_binaries/matitaprover/TreeLimitedRun.c b/...ts/binaries/matitaprover/TreeLimitedRun.c → ...en_binaries/matitaprover/TreeLimitedRun.c
diff --git a/components/binaries/matitaprover/Veloci → ...nents/broken_binaries/matitaprover/Veloci b/components/binaries/matitaprover/Veloci → ...nents/broken_binaries/matitaprover/Veloci
diff --git a/components/binaries/matitaprover/_tags → ...onents/broken_binaries/matitaprover/_tags b/components/binaries/matitaprover/_tags → ...onents/broken_binaries/matitaprover/_tags
diff --git a/components/binaries/matitaprover/ast.ml → ...nents/broken_binaries/matitaprover/ast.ml b/components/binaries/matitaprover/ast.ml → ...nents/broken_binaries/matitaprover/ast.ml
diff --git a/.../matitaprover/benchmarks/andrea_log090729 → .../matitaprover/benchmarks/andrea_log090729 b/.../matitaprover/benchmarks/andrea_log090729 → .../matitaprover/benchmarks/andrea_log090729
diff --git a/...naries/matitaprover/benchmarks/log.090625 → ...naries/matitaprover/benchmarks/log.090625 b/...naries/matitaprover/benchmarks/log.090625 → ...naries/matitaprover/benchmarks/log.090625
diff --git a/...naries/matitaprover/benchmarks/log.090627 → ...naries/matitaprover/benchmarks/log.090627 b/...naries/matitaprover/benchmarks/log.090627 → ...naries/matitaprover/benchmarks/log.090627
diff --git a/...naries/matitaprover/benchmarks/log.090629 → ...naries/matitaprover/benchmarks/log.090629 b/...naries/matitaprover/benchmarks/log.090629 → ...naries/matitaprover/benchmarks/log.090629
diff --git a/...ks/log.090629-no-infer-on-closed-goals-10 → ...ks/log.090629-no-infer-on-closed-goals-10 b/...ks/log.090629-no-infer-on-closed-goals-10 → ...ks/log.090629-no-infer-on-closed-goals-10
diff --git a/...itaprover/benchmarks/log.180CPU.reference → ...itaprover/benchmarks/log.180CPU.reference b/...itaprover/benchmarks/log.180CPU.reference → ...itaprover/benchmarks/log.180CPU.reference
diff --git a/...atitaprover/benchmarks/log.90.fixed-order → ...atitaprover/benchmarks/log.90.fixed-order b/...atitaprover/benchmarks/log.90.fixed-order → ...atitaprover/benchmarks/log.90.fixed-order
diff --git a/...itaprover/benchmarks/log.90.fixed-order.2 → ...itaprover/benchmarks/log.90.fixed-order.2 b/...itaprover/benchmarks/log.90.fixed-order.2 → ...itaprover/benchmarks/log.90.fixed-order.2
diff --git a/...arks/log.90.reference.submitted.CASC.2009 → ...arks/log.90.reference.submitted.CASC.2009 b/...arks/log.90.reference.submitted.CASC.2009 → ...arks/log.90.reference.submitted.CASC.2009
diff --git a/components/binaries/matitaprover/casc_2008 → ...ts/broken_binaries/matitaprover/casc_2008 b/components/binaries/matitaprover/casc_2008 → ...ts/broken_binaries/matitaprover/casc_2008
diff --git a/...aries/matitaprover/discrimination_tree.ml → ...aries/matitaprover/discrimination_tree.ml b/...aries/matitaprover/discrimination_tree.ml → ...aries/matitaprover/discrimination_tree.ml
diff --git a/...ries/matitaprover/discrimination_tree.mli → ...ries/matitaprover/discrimination_tree.mli b/...ries/matitaprover/discrimination_tree.mli → ...ries/matitaprover/discrimination_tree.mli
diff --git a/...itaprover/eligible_unit_equality_problems → ...itaprover/eligible_unit_equality_problems b/...itaprover/eligible_unit_equality_problems → ...itaprover/eligible_unit_equality_problems
diff --git a/components/binaries/matitaprover/foSubst.ml → ...s/broken_binaries/matitaprover/foSubst.ml b/components/binaries/matitaprover/foSubst.ml → ...s/broken_binaries/matitaprover/foSubst.ml
diff --git a/components/binaries/matitaprover/foSubst.mli → .../broken_binaries/matitaprover/foSubst.mli b/components/binaries/matitaprover/foSubst.mli → .../broken_binaries/matitaprover/foSubst.mli
diff --git a/components/binaries/matitaprover/foUnif.ml → ...ts/broken_binaries/matitaprover/foUnif.ml b/components/binaries/matitaprover/foUnif.ml → ...ts/broken_binaries/matitaprover/foUnif.ml
diff --git a/components/binaries/matitaprover/foUnif.mli → ...s/broken_binaries/matitaprover/foUnif.mli b/components/binaries/matitaprover/foUnif.mli → ...s/broken_binaries/matitaprover/foUnif.mli
diff --git a/components/binaries/matitaprover/foUtils.ml → ...s/broken_binaries/matitaprover/foUtils.ml b/components/binaries/matitaprover/foUtils.ml → ...s/broken_binaries/matitaprover/foUtils.ml
diff --git a/components/binaries/matitaprover/foUtils.mli → .../broken_binaries/matitaprover/foUtils.mli b/components/binaries/matitaprover/foUtils.mli → .../broken_binaries/matitaprover/foUtils.mli
diff --git a/components/binaries/matitaprover/hExtlib.ml → ...s/broken_binaries/matitaprover/hExtlib.ml b/components/binaries/matitaprover/hExtlib.ml → ...s/broken_binaries/matitaprover/hExtlib.ml
diff --git a/components/binaries/matitaprover/hExtlib.mli → .../broken_binaries/matitaprover/hExtlib.mli b/components/binaries/matitaprover/hExtlib.mli → .../broken_binaries/matitaprover/hExtlib.mli
diff --git a/...onents/binaries/matitaprover/hTopoSort.ml → ...broken_binaries/matitaprover/hTopoSort.ml b/...onents/binaries/matitaprover/hTopoSort.ml → ...broken_binaries/matitaprover/hTopoSort.ml
diff --git a/...nents/binaries/matitaprover/hTopoSort.mli → ...roken_binaries/matitaprover/hTopoSort.mli b/...nents/binaries/matitaprover/hTopoSort.mli → ...roken_binaries/matitaprover/hTopoSort.mli
diff --git a/components/binaries/matitaprover/index.ml → ...nts/broken_binaries/matitaprover/index.ml b/components/binaries/matitaprover/index.ml → ...nts/broken_binaries/matitaprover/index.ml
diff --git a/components/binaries/matitaprover/index.mli → ...ts/broken_binaries/matitaprover/index.mli b/components/binaries/matitaprover/index.mli → ...ts/broken_binaries/matitaprover/index.mli
diff --git a/components/binaries/matitaprover/lexer.mll → ...ts/broken_binaries/matitaprover/lexer.mll b/components/binaries/matitaprover/lexer.mll → ...ts/broken_binaries/matitaprover/lexer.mll
diff --git a/...nts/binaries/matitaprover/matitaprover.ml → ...ken_binaries/matitaprover/matitaprover.ml b/...nts/binaries/matitaprover/matitaprover.ml → ...ken_binaries/matitaprover/matitaprover.ml
diff --git a/...onents/binaries/matitaprover/orderings.ml → ...broken_binaries/matitaprover/orderings.ml b/...onents/binaries/matitaprover/orderings.ml → ...broken_binaries/matitaprover/orderings.ml
diff --git a/...nents/binaries/matitaprover/orderings.mli → ...roken_binaries/matitaprover/orderings.mli b/...nents/binaries/matitaprover/orderings.mli → ...roken_binaries/matitaprover/orderings.mli
diff --git a/components/binaries/matitaprover/paramod.ml → ...s/broken_binaries/matitaprover/paramod.ml b/components/binaries/matitaprover/paramod.ml → ...s/broken_binaries/matitaprover/paramod.ml
diff --git a/components/binaries/matitaprover/paramod.mli → .../broken_binaries/matitaprover/paramod.mli b/components/binaries/matitaprover/paramod.mli → .../broken_binaries/matitaprover/paramod.mli
diff --git a/components/binaries/matitaprover/parser.mly → ...s/broken_binaries/matitaprover/parser.mly b/components/binaries/matitaprover/parser.mly → ...s/broken_binaries/matitaprover/parser.mly
diff --git a/components/binaries/matitaprover/pp.ml → ...onents/broken_binaries/matitaprover/pp.ml b/components/binaries/matitaprover/pp.ml → ...onents/broken_binaries/matitaprover/pp.ml
diff --git a/components/binaries/matitaprover/pp.mli → ...nents/broken_binaries/matitaprover/pp.mli b/components/binaries/matitaprover/pp.mli → ...nents/broken_binaries/matitaprover/pp.mli
diff --git a/...ts/binaries/matitaprover/run_on_a_list.sh → ...en_binaries/matitaprover/run_on_a_list.sh b/...ts/binaries/matitaprover/run_on_a_list.sh → ...en_binaries/matitaprover/run_on_a_list.sh
diff --git a/components/binaries/matitaprover/stats.ml → ...nts/broken_binaries/matitaprover/stats.ml b/components/binaries/matitaprover/stats.ml → ...nts/broken_binaries/matitaprover/stats.ml
diff --git a/components/binaries/matitaprover/stats.mli → ...ts/broken_binaries/matitaprover/stats.mli b/components/binaries/matitaprover/stats.mli → ...ts/broken_binaries/matitaprover/stats.mli
diff --git a/components/binaries/matitaprover/stdpp.ml → ...nts/broken_binaries/matitaprover/stdpp.ml b/components/binaries/matitaprover/stdpp.ml → ...nts/broken_binaries/matitaprover/stdpp.ml
diff --git a/components/binaries/matitaprover/sum_up.awk → ...s/broken_binaries/matitaprover/sum_up.awk b/components/binaries/matitaprover/sum_up.awk → ...s/broken_binaries/matitaprover/sum_up.awk
diff --git a/...ts/binaries/matitaprover/superposition.ml → ...en_binaries/matitaprover/superposition.ml b/...ts/binaries/matitaprover/superposition.ml → ...en_binaries/matitaprover/superposition.ml
diff --git a/...s/binaries/matitaprover/superposition.mli → ...n_binaries/matitaprover/superposition.mli b/...s/binaries/matitaprover/superposition.mli → ...n_binaries/matitaprover/superposition.mli
diff --git a/components/binaries/matitaprover/terms.ml → ...nts/broken_binaries/matitaprover/terms.ml b/components/binaries/matitaprover/terms.ml → ...nts/broken_binaries/matitaprover/terms.ml
diff --git a/components/binaries/matitaprover/terms.mli → ...ts/broken_binaries/matitaprover/terms.mli b/components/binaries/matitaprover/terms.mli → ...ts/broken_binaries/matitaprover/terms.mli
diff --git a/components/binaries/matitaprover/tptp_cnf.ml → .../broken_binaries/matitaprover/tptp_cnf.ml b/components/binaries/matitaprover/tptp_cnf.ml → .../broken_binaries/matitaprover/tptp_cnf.ml
diff --git a/...onents/binaries/matitaprover/tptp_cnf.mli → ...broken_binaries/matitaprover/tptp_cnf.mli b/...onents/binaries/matitaprover/tptp_cnf.mli → ...broken_binaries/matitaprover/tptp_cnf.mli
diff --git a/components/binaries/matitaprover/trie.ml → ...ents/broken_binaries/matitaprover/trie.ml b/components/binaries/matitaprover/trie.ml → ...ents/broken_binaries/matitaprover/trie.ml
diff --git a/components/binaries/matitaprover/trie.mli → ...nts/broken_binaries/matitaprover/trie.mli b/components/binaries/matitaprover/trie.mli → ...nts/broken_binaries/matitaprover/trie.mli
diff --git a/components/binaries/saturate/Makefile → components/broken_binaries/saturate/Makefile b/components/binaries/saturate/Makefile → components/broken_binaries/saturate/Makefile
diff --git a/...onents/binaries/saturate/saturate_main.ml → ...broken_binaries/saturate/saturate_main.ml b/...onents/binaries/saturate/saturate_main.ml → ...broken_binaries/saturate/saturate_main.ml
diff --git a/components/binaries/test_lexer/Makefile → ...nents/broken_binaries/test_lexer/Makefile b/components/binaries/test_lexer/Makefile → ...nents/broken_binaries/test_lexer/Makefile
diff --git a/components/binaries/test_lexer/test_lexer.ml → .../broken_binaries/test_lexer/test_lexer.ml b/components/binaries/test_lexer/test_lexer.ml → .../broken_binaries/test_lexer/test_lexer.ml
diff --git a/components/binaries/test_parser/Makefile → ...ents/broken_binaries/test_parser/Makefile b/components/binaries/test_parser/Makefile → ...ents/broken_binaries/test_parser/Makefile
diff --git a/components/binaries/test_parser/test_dep.ml → ...s/broken_binaries/test_parser/test_dep.ml b/components/binaries/test_parser/test_dep.ml → ...s/broken_binaries/test_parser/test_dep.ml
diff --git a/...nents/binaries/test_parser/test_parser.ml → ...roken_binaries/test_parser/test_parser.ml b/...nents/binaries/test_parser/test_parser.ml → ...roken_binaries/test_parser/test_parser.ml
diff --git a/matita.install b/matita.install
@@ -93,22 +93,36 @@ share_root: [
   "_build/install/default/share/matita/myshare/lib/basics/core_notation.ma" {"matita/myshare/lib/basics/core_notation.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/apart_2.ma" {"matita/myshare/lib/basics/core_notation/apart_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/card_1.ma" {"matita/myshare/lib/basics/core_notation/card_1.ma"}
-  "_build/install/default/share/matita/myshare/lib/basics/core_notation/compose_2.ma" {"matita/myshare/lib/basics/core_notation/compose_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/complexes_0.ma" {"matita/myshare/lib/basics/core_notation/complexes_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/compose_5.ma" {"matita/myshare/lib/basics/core_notation/compose_5.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/comprehension_2.ma" {"matita/myshare/lib/basics/core_notation/comprehension_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/downarrow_1.ma" {"matita/myshare/lib/basics/core_notation/downarrow_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/eq_3.ma" {"matita/myshare/lib/basics/core_notation/eq_3.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/exp_2.ma" {"matita/myshare/lib/basics/core_notation/exp_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/fact_1.ma" {"matita/myshare/lib/basics/core_notation/fact_1.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/fintersects_2.ma" {"matita/myshare/lib/basics/core_notation/fintersects_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/funion_2.ma" {"matita/myshare/lib/basics/core_notation/funion_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/hide_1.ma" {"matita/myshare/lib/basics/core_notation/hide_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/imply_2.ma" {"matita/myshare/lib/basics/core_notation/imply_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/integers_0.ma" {"matita/myshare/lib/basics/core_notation/integers_0.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/invert_1.ma" {"matita/myshare/lib/basics/core_notation/invert_1.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/invert_appl_2.ma" {"matita/myshare/lib/basics/core_notation/invert_appl_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/napart_2.ma" {"matita/myshare/lib/basics/core_notation/napart_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/naturals_0.ma" {"matita/myshare/lib/basics/core_notation/naturals_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/neutral_0.ma" {"matita/myshare/lib/basics/core_notation/neutral_0.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/overlaps_2.ma" {"matita/myshare/lib/basics/core_notation/overlaps_2.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/pair_2.ma" {"matita/myshare/lib/basics/core_notation/pair_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/product_2.ma" {"matita/myshare/lib/basics/core_notation/product_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/rationals_0.ma" {"matita/myshare/lib/basics/core_notation/rationals_0.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/reals_0.ma" {"matita/myshare/lib/basics/core_notation/reals_0.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/singl_1.ma" {"matita/myshare/lib/basics/core_notation/singl_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/sqrt_1.ma" {"matita/myshare/lib/basics/core_notation/sqrt_1.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/subset_1.ma" {"matita/myshare/lib/basics/core_notation/subset_1.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/subseteq_2.ma" {"matita/myshare/lib/basics/core_notation/subseteq_2.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/uminus_1.ma" {"matita/myshare/lib/basics/core_notation/uminus_1.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/core_notation/uparrow_1.ma" {"matita/myshare/lib/basics/core_notation/uparrow_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/vdash_1.ma" {"matita/myshare/lib/basics/core_notation/vdash_1.ma"}
+  "_build/install/default/share/matita/myshare/lib/basics/core_notation/vdash_3.ma" {"matita/myshare/lib/basics/core_notation/vdash_3.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/deqlist.ma" {"matita/myshare/lib/basics/deqlist.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/deqsets.ma" {"matita/myshare/lib/basics/deqsets.ma"}
   "_build/install/default/share/matita/myshare/lib/basics/finset.ma" {"matita/myshare/lib/basics/finset.ma"}