From c952d47105bc6234bf009f1c9363aeda857ff2fe Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Sep 2023 16:17:50 +0200 Subject: [PATCH 1/2] Move broken binaries into broken_binaries Also document in the Makefile what the remaining binaries do. They are all maintained by Ferruccio Guidi --- components/binaries/Makefile | 8 +++--- components/broken_binaries/Makefile | 18 +++++++++++++ components/broken_binaries/Makefile.common | 25 +++++++++++++++++++ .../dump_db/dump.sh | 0 .../matitaprover/CASC_2008 | 0 .../matitaprover/FIXME | 0 .../matitaprover/Makefile | 0 .../matitaprover/SystemDescriptionMatita.html | 0 .../matitaprover/TreeLimitedRun.c | 0 .../matitaprover/Veloci | 0 .../matitaprover/_tags | 0 .../matitaprover/ast.ml | 0 .../matitaprover/benchmarks/andrea_log090729 | 0 .../matitaprover/benchmarks/log.090625 | 0 .../matitaprover/benchmarks/log.090627 | 0 .../matitaprover/benchmarks/log.090629 | 0 .../log.090629-no-infer-on-closed-goals-10 | 0 .../benchmarks/log.180CPU.reference | 0 .../benchmarks/log.90.fixed-order | 0 .../benchmarks/log.90.fixed-order.2 | 0 .../log.90.reference.submitted.CASC.2009 | 0 .../matitaprover/casc_2008 | 0 .../matitaprover/discrimination_tree.ml | 0 .../matitaprover/discrimination_tree.mli | 0 .../eligible_unit_equality_problems | 0 .../matitaprover/foSubst.ml | 0 .../matitaprover/foSubst.mli | 0 .../matitaprover/foUnif.ml | 0 .../matitaprover/foUnif.mli | 0 .../matitaprover/foUtils.ml | 0 .../matitaprover/foUtils.mli | 0 .../matitaprover/hExtlib.ml | 0 .../matitaprover/hExtlib.mli | 0 .../matitaprover/hTopoSort.ml | 0 .../matitaprover/hTopoSort.mli | 0 .../matitaprover/index.ml | 0 .../matitaprover/index.mli | 0 .../matitaprover/lexer.mll | 0 .../matitaprover/matitaprover.ml | 0 .../matitaprover/orderings.ml | 0 .../matitaprover/orderings.mli | 0 .../matitaprover/paramod.ml | 0 .../matitaprover/paramod.mli | 0 .../matitaprover/parser.mly | 0 .../matitaprover/pp.ml | 0 .../matitaprover/pp.mli | 0 .../matitaprover/run_on_a_list.sh | 0 .../matitaprover/stats.ml | 0 .../matitaprover/stats.mli | 0 .../matitaprover/stdpp.ml | 0 .../matitaprover/sum_up.awk | 0 .../matitaprover/superposition.ml | 0 .../matitaprover/superposition.mli | 0 .../matitaprover/terms.ml | 0 .../matitaprover/terms.mli | 0 .../matitaprover/tptp_cnf.ml | 0 .../matitaprover/tptp_cnf.mli | 0 .../matitaprover/trie.ml | 0 .../matitaprover/trie.mli | 0 .../saturate/Makefile | 0 .../saturate/saturate_main.ml | 0 .../test_lexer/Makefile | 0 .../test_lexer/test_lexer.ml | 0 .../test_parser/Makefile | 0 .../test_parser/test_dep.ml | 0 .../test_parser/test_parser.ml | 0 66 files changed, 47 insertions(+), 4 deletions(-) create mode 100644 components/broken_binaries/Makefile create mode 100644 components/broken_binaries/Makefile.common rename components/{binaries => broken_binaries}/dump_db/dump.sh (100%) rename components/{binaries => broken_binaries}/matitaprover/CASC_2008 (100%) rename components/{binaries => broken_binaries}/matitaprover/FIXME (100%) rename components/{binaries => broken_binaries}/matitaprover/Makefile (100%) rename components/{binaries => broken_binaries}/matitaprover/SystemDescriptionMatita.html (100%) rename components/{binaries => broken_binaries}/matitaprover/TreeLimitedRun.c (100%) rename components/{binaries => broken_binaries}/matitaprover/Veloci (100%) rename components/{binaries => broken_binaries}/matitaprover/_tags (100%) rename components/{binaries => broken_binaries}/matitaprover/ast.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/andrea_log090729 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.090625 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.090627 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.090629 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.180CPU.reference (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.90.fixed-order (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.90.fixed-order.2 (100%) rename components/{binaries => broken_binaries}/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 (100%) rename components/{binaries => broken_binaries}/matitaprover/casc_2008 (100%) rename components/{binaries => broken_binaries}/matitaprover/discrimination_tree.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/discrimination_tree.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/eligible_unit_equality_problems (100%) rename components/{binaries => broken_binaries}/matitaprover/foSubst.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/foSubst.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/foUnif.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/foUnif.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/foUtils.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/foUtils.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/hExtlib.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/hExtlib.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/hTopoSort.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/hTopoSort.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/index.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/index.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/lexer.mll (100%) rename components/{binaries => broken_binaries}/matitaprover/matitaprover.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/orderings.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/orderings.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/paramod.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/paramod.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/parser.mly (100%) rename components/{binaries => broken_binaries}/matitaprover/pp.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/pp.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/run_on_a_list.sh (100%) rename components/{binaries => broken_binaries}/matitaprover/stats.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/stats.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/stdpp.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/sum_up.awk (100%) rename components/{binaries => broken_binaries}/matitaprover/superposition.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/superposition.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/terms.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/terms.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/tptp_cnf.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/tptp_cnf.mli (100%) rename components/{binaries => broken_binaries}/matitaprover/trie.ml (100%) rename components/{binaries => broken_binaries}/matitaprover/trie.mli (100%) rename components/{binaries => broken_binaries}/saturate/Makefile (100%) rename components/{binaries => broken_binaries}/saturate/saturate_main.ml (100%) rename components/{binaries => broken_binaries}/test_lexer/Makefile (100%) rename components/{binaries => broken_binaries}/test_lexer/test_lexer.ml (100%) rename components/{binaries => broken_binaries}/test_parser/Makefile (100%) rename components/{binaries => broken_binaries}/test_parser/test_dep.ml (100%) rename components/{binaries => broken_binaries}/test_parser/test_parser.ml (100%) diff --git a/components/binaries/Makefile b/components/binaries/Makefile index 2f2faf326..382bf77db 100644 --- 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 new file mode 100644 index 000000000..893328c4f --- /dev/null +++ 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:%=rec@depend.opt@%) +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 new file mode 100644 index 000000000..78733ed39 --- /dev/null +++ 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 b/components/broken_binaries/dump_db/dump.sh similarity index 100% rename from components/binaries/dump_db/dump.sh rename to components/broken_binaries/dump_db/dump.sh diff --git a/components/binaries/matitaprover/CASC_2008 b/components/broken_binaries/matitaprover/CASC_2008 similarity index 100% rename from components/binaries/matitaprover/CASC_2008 rename to components/broken_binaries/matitaprover/CASC_2008 diff --git a/components/binaries/matitaprover/FIXME b/components/broken_binaries/matitaprover/FIXME similarity index 100% rename from components/binaries/matitaprover/FIXME rename to components/broken_binaries/matitaprover/FIXME diff --git a/components/binaries/matitaprover/Makefile b/components/broken_binaries/matitaprover/Makefile similarity index 100% rename from components/binaries/matitaprover/Makefile rename to components/broken_binaries/matitaprover/Makefile diff --git a/components/binaries/matitaprover/SystemDescriptionMatita.html b/components/broken_binaries/matitaprover/SystemDescriptionMatita.html similarity index 100% rename from components/binaries/matitaprover/SystemDescriptionMatita.html rename to components/broken_binaries/matitaprover/SystemDescriptionMatita.html diff --git a/components/binaries/matitaprover/TreeLimitedRun.c b/components/broken_binaries/matitaprover/TreeLimitedRun.c similarity index 100% rename from components/binaries/matitaprover/TreeLimitedRun.c rename to components/broken_binaries/matitaprover/TreeLimitedRun.c diff --git a/components/binaries/matitaprover/Veloci b/components/broken_binaries/matitaprover/Veloci similarity index 100% rename from components/binaries/matitaprover/Veloci rename to components/broken_binaries/matitaprover/Veloci diff --git a/components/binaries/matitaprover/_tags b/components/broken_binaries/matitaprover/_tags similarity index 100% rename from components/binaries/matitaprover/_tags rename to components/broken_binaries/matitaprover/_tags diff --git a/components/binaries/matitaprover/ast.ml b/components/broken_binaries/matitaprover/ast.ml similarity index 100% rename from components/binaries/matitaprover/ast.ml rename to components/broken_binaries/matitaprover/ast.ml diff --git a/components/binaries/matitaprover/benchmarks/andrea_log090729 b/components/broken_binaries/matitaprover/benchmarks/andrea_log090729 similarity index 100% rename from components/binaries/matitaprover/benchmarks/andrea_log090729 rename to components/broken_binaries/matitaprover/benchmarks/andrea_log090729 diff --git a/components/binaries/matitaprover/benchmarks/log.090625 b/components/broken_binaries/matitaprover/benchmarks/log.090625 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090625 rename to components/broken_binaries/matitaprover/benchmarks/log.090625 diff --git a/components/binaries/matitaprover/benchmarks/log.090627 b/components/broken_binaries/matitaprover/benchmarks/log.090627 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090627 rename to components/broken_binaries/matitaprover/benchmarks/log.090627 diff --git a/components/binaries/matitaprover/benchmarks/log.090629 b/components/broken_binaries/matitaprover/benchmarks/log.090629 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090629 rename to components/broken_binaries/matitaprover/benchmarks/log.090629 diff --git a/components/binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 b/components/broken_binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 rename to components/broken_binaries/matitaprover/benchmarks/log.090629-no-infer-on-closed-goals-10 diff --git a/components/binaries/matitaprover/benchmarks/log.180CPU.reference b/components/broken_binaries/matitaprover/benchmarks/log.180CPU.reference similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.180CPU.reference rename to components/broken_binaries/matitaprover/benchmarks/log.180CPU.reference diff --git a/components/binaries/matitaprover/benchmarks/log.90.fixed-order b/components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.fixed-order rename to components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order diff --git a/components/binaries/matitaprover/benchmarks/log.90.fixed-order.2 b/components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order.2 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.fixed-order.2 rename to components/broken_binaries/matitaprover/benchmarks/log.90.fixed-order.2 diff --git a/components/binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 b/components/broken_binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 similarity index 100% rename from components/binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 rename to components/broken_binaries/matitaprover/benchmarks/log.90.reference.submitted.CASC.2009 diff --git a/components/binaries/matitaprover/casc_2008 b/components/broken_binaries/matitaprover/casc_2008 similarity index 100% rename from components/binaries/matitaprover/casc_2008 rename to components/broken_binaries/matitaprover/casc_2008 diff --git a/components/binaries/matitaprover/discrimination_tree.ml b/components/broken_binaries/matitaprover/discrimination_tree.ml similarity index 100% rename from components/binaries/matitaprover/discrimination_tree.ml rename to components/broken_binaries/matitaprover/discrimination_tree.ml diff --git a/components/binaries/matitaprover/discrimination_tree.mli b/components/broken_binaries/matitaprover/discrimination_tree.mli similarity index 100% rename from components/binaries/matitaprover/discrimination_tree.mli rename to components/broken_binaries/matitaprover/discrimination_tree.mli diff --git a/components/binaries/matitaprover/eligible_unit_equality_problems b/components/broken_binaries/matitaprover/eligible_unit_equality_problems similarity index 100% rename from components/binaries/matitaprover/eligible_unit_equality_problems rename to components/broken_binaries/matitaprover/eligible_unit_equality_problems diff --git a/components/binaries/matitaprover/foSubst.ml b/components/broken_binaries/matitaprover/foSubst.ml similarity index 100% rename from components/binaries/matitaprover/foSubst.ml rename to components/broken_binaries/matitaprover/foSubst.ml diff --git a/components/binaries/matitaprover/foSubst.mli b/components/broken_binaries/matitaprover/foSubst.mli similarity index 100% rename from components/binaries/matitaprover/foSubst.mli rename to components/broken_binaries/matitaprover/foSubst.mli diff --git a/components/binaries/matitaprover/foUnif.ml b/components/broken_binaries/matitaprover/foUnif.ml similarity index 100% rename from components/binaries/matitaprover/foUnif.ml rename to components/broken_binaries/matitaprover/foUnif.ml diff --git a/components/binaries/matitaprover/foUnif.mli b/components/broken_binaries/matitaprover/foUnif.mli similarity index 100% rename from components/binaries/matitaprover/foUnif.mli rename to components/broken_binaries/matitaprover/foUnif.mli diff --git a/components/binaries/matitaprover/foUtils.ml b/components/broken_binaries/matitaprover/foUtils.ml similarity index 100% rename from components/binaries/matitaprover/foUtils.ml rename to components/broken_binaries/matitaprover/foUtils.ml diff --git a/components/binaries/matitaprover/foUtils.mli b/components/broken_binaries/matitaprover/foUtils.mli similarity index 100% rename from components/binaries/matitaprover/foUtils.mli rename to components/broken_binaries/matitaprover/foUtils.mli diff --git a/components/binaries/matitaprover/hExtlib.ml b/components/broken_binaries/matitaprover/hExtlib.ml similarity index 100% rename from components/binaries/matitaprover/hExtlib.ml rename to components/broken_binaries/matitaprover/hExtlib.ml diff --git a/components/binaries/matitaprover/hExtlib.mli b/components/broken_binaries/matitaprover/hExtlib.mli similarity index 100% rename from components/binaries/matitaprover/hExtlib.mli rename to components/broken_binaries/matitaprover/hExtlib.mli diff --git a/components/binaries/matitaprover/hTopoSort.ml b/components/broken_binaries/matitaprover/hTopoSort.ml similarity index 100% rename from components/binaries/matitaprover/hTopoSort.ml rename to components/broken_binaries/matitaprover/hTopoSort.ml diff --git a/components/binaries/matitaprover/hTopoSort.mli b/components/broken_binaries/matitaprover/hTopoSort.mli similarity index 100% rename from components/binaries/matitaprover/hTopoSort.mli rename to components/broken_binaries/matitaprover/hTopoSort.mli diff --git a/components/binaries/matitaprover/index.ml b/components/broken_binaries/matitaprover/index.ml similarity index 100% rename from components/binaries/matitaprover/index.ml rename to components/broken_binaries/matitaprover/index.ml diff --git a/components/binaries/matitaprover/index.mli b/components/broken_binaries/matitaprover/index.mli similarity index 100% rename from components/binaries/matitaprover/index.mli rename to components/broken_binaries/matitaprover/index.mli diff --git a/components/binaries/matitaprover/lexer.mll b/components/broken_binaries/matitaprover/lexer.mll similarity index 100% rename from components/binaries/matitaprover/lexer.mll rename to components/broken_binaries/matitaprover/lexer.mll diff --git a/components/binaries/matitaprover/matitaprover.ml b/components/broken_binaries/matitaprover/matitaprover.ml similarity index 100% rename from components/binaries/matitaprover/matitaprover.ml rename to components/broken_binaries/matitaprover/matitaprover.ml diff --git a/components/binaries/matitaprover/orderings.ml b/components/broken_binaries/matitaprover/orderings.ml similarity index 100% rename from components/binaries/matitaprover/orderings.ml rename to components/broken_binaries/matitaprover/orderings.ml diff --git a/components/binaries/matitaprover/orderings.mli b/components/broken_binaries/matitaprover/orderings.mli similarity index 100% rename from components/binaries/matitaprover/orderings.mli rename to components/broken_binaries/matitaprover/orderings.mli diff --git a/components/binaries/matitaprover/paramod.ml b/components/broken_binaries/matitaprover/paramod.ml similarity index 100% rename from components/binaries/matitaprover/paramod.ml rename to components/broken_binaries/matitaprover/paramod.ml diff --git a/components/binaries/matitaprover/paramod.mli b/components/broken_binaries/matitaprover/paramod.mli similarity index 100% rename from components/binaries/matitaprover/paramod.mli rename to components/broken_binaries/matitaprover/paramod.mli diff --git a/components/binaries/matitaprover/parser.mly b/components/broken_binaries/matitaprover/parser.mly similarity index 100% rename from components/binaries/matitaprover/parser.mly rename to components/broken_binaries/matitaprover/parser.mly diff --git a/components/binaries/matitaprover/pp.ml b/components/broken_binaries/matitaprover/pp.ml similarity index 100% rename from components/binaries/matitaprover/pp.ml rename to components/broken_binaries/matitaprover/pp.ml diff --git a/components/binaries/matitaprover/pp.mli b/components/broken_binaries/matitaprover/pp.mli similarity index 100% rename from components/binaries/matitaprover/pp.mli rename to components/broken_binaries/matitaprover/pp.mli diff --git a/components/binaries/matitaprover/run_on_a_list.sh b/components/broken_binaries/matitaprover/run_on_a_list.sh similarity index 100% rename from components/binaries/matitaprover/run_on_a_list.sh rename to components/broken_binaries/matitaprover/run_on_a_list.sh diff --git a/components/binaries/matitaprover/stats.ml b/components/broken_binaries/matitaprover/stats.ml similarity index 100% rename from components/binaries/matitaprover/stats.ml rename to components/broken_binaries/matitaprover/stats.ml diff --git a/components/binaries/matitaprover/stats.mli b/components/broken_binaries/matitaprover/stats.mli similarity index 100% rename from components/binaries/matitaprover/stats.mli rename to components/broken_binaries/matitaprover/stats.mli diff --git a/components/binaries/matitaprover/stdpp.ml b/components/broken_binaries/matitaprover/stdpp.ml similarity index 100% rename from components/binaries/matitaprover/stdpp.ml rename to components/broken_binaries/matitaprover/stdpp.ml diff --git a/components/binaries/matitaprover/sum_up.awk b/components/broken_binaries/matitaprover/sum_up.awk similarity index 100% rename from components/binaries/matitaprover/sum_up.awk rename to components/broken_binaries/matitaprover/sum_up.awk diff --git a/components/binaries/matitaprover/superposition.ml b/components/broken_binaries/matitaprover/superposition.ml similarity index 100% rename from components/binaries/matitaprover/superposition.ml rename to components/broken_binaries/matitaprover/superposition.ml diff --git a/components/binaries/matitaprover/superposition.mli b/components/broken_binaries/matitaprover/superposition.mli similarity index 100% rename from components/binaries/matitaprover/superposition.mli rename to components/broken_binaries/matitaprover/superposition.mli diff --git a/components/binaries/matitaprover/terms.ml b/components/broken_binaries/matitaprover/terms.ml similarity index 100% rename from components/binaries/matitaprover/terms.ml rename to components/broken_binaries/matitaprover/terms.ml diff --git a/components/binaries/matitaprover/terms.mli b/components/broken_binaries/matitaprover/terms.mli similarity index 100% rename from components/binaries/matitaprover/terms.mli rename to components/broken_binaries/matitaprover/terms.mli diff --git a/components/binaries/matitaprover/tptp_cnf.ml b/components/broken_binaries/matitaprover/tptp_cnf.ml similarity index 100% rename from components/binaries/matitaprover/tptp_cnf.ml rename to components/broken_binaries/matitaprover/tptp_cnf.ml diff --git a/components/binaries/matitaprover/tptp_cnf.mli b/components/broken_binaries/matitaprover/tptp_cnf.mli similarity index 100% rename from components/binaries/matitaprover/tptp_cnf.mli rename to components/broken_binaries/matitaprover/tptp_cnf.mli diff --git a/components/binaries/matitaprover/trie.ml b/components/broken_binaries/matitaprover/trie.ml similarity index 100% rename from components/binaries/matitaprover/trie.ml rename to components/broken_binaries/matitaprover/trie.ml diff --git a/components/binaries/matitaprover/trie.mli b/components/broken_binaries/matitaprover/trie.mli similarity index 100% rename from components/binaries/matitaprover/trie.mli rename to components/broken_binaries/matitaprover/trie.mli diff --git a/components/binaries/saturate/Makefile b/components/broken_binaries/saturate/Makefile similarity index 100% rename from components/binaries/saturate/Makefile rename to components/broken_binaries/saturate/Makefile diff --git a/components/binaries/saturate/saturate_main.ml b/components/broken_binaries/saturate/saturate_main.ml similarity index 100% rename from components/binaries/saturate/saturate_main.ml rename to components/broken_binaries/saturate/saturate_main.ml diff --git a/components/binaries/test_lexer/Makefile b/components/broken_binaries/test_lexer/Makefile similarity index 100% rename from components/binaries/test_lexer/Makefile rename to components/broken_binaries/test_lexer/Makefile diff --git a/components/binaries/test_lexer/test_lexer.ml b/components/broken_binaries/test_lexer/test_lexer.ml similarity index 100% rename from components/binaries/test_lexer/test_lexer.ml rename to components/broken_binaries/test_lexer/test_lexer.ml diff --git a/components/binaries/test_parser/Makefile b/components/broken_binaries/test_parser/Makefile similarity index 100% rename from components/binaries/test_parser/Makefile rename to components/broken_binaries/test_parser/Makefile diff --git a/components/binaries/test_parser/test_dep.ml b/components/broken_binaries/test_parser/test_dep.ml similarity index 100% rename from components/binaries/test_parser/test_dep.ml rename to components/broken_binaries/test_parser/test_dep.ml diff --git a/components/binaries/test_parser/test_parser.ml b/components/broken_binaries/test_parser/test_parser.ml similarity index 100% rename from components/binaries/test_parser/test_parser.ml rename to components/broken_binaries/test_parser/test_parser.ml From 71b993b8b9a1bca5df03dcaf964764f0460025ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Sep 2023 16:18:06 +0200 Subject: [PATCH 2/2] regenerated --- matita.install | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/matita.install b/matita.install index b37e55e1e..658000ffd 100644 --- 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"}