From 37d26b580805b10be73ed4a0480d4c2527d88fbc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 22 Jul 2024 13:16:33 +0200 Subject: [PATCH] Remove generated files --- erasure-plugin/clean_extraction.sh | 2 +- safechecker-plugin/clean_extraction.sh | 2 +- template-coq/_PluginProject | 248 ------------------------- template-coq/_TemplateCoqProject | 32 ---- 4 files changed, 2 insertions(+), 282 deletions(-) delete mode 100644 template-coq/_PluginProject delete mode 100644 template-coq/_TemplateCoqProject diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh index 4187f6ddc..562a941fa 100755 --- a/erasure-plugin/clean_extraction.sh +++ b/erasure-plugin/clean_extraction.sh @@ -9,7 +9,7 @@ fi shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files -files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` +files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` if [[ ! -f "src/metacoq_erasure_plugin.cmxs" || "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]] diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh index 44164597f..85e2f761a 100755 --- a/safechecker-plugin/clean_extraction.sh +++ b/safechecker-plugin/clean_extraction.sh @@ -9,7 +9,7 @@ fi shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files -files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` +files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/` if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" || "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]] diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject deleted file mode 100644 index 314e020ac..000000000 --- a/template-coq/_PluginProject +++ /dev/null @@ -1,248 +0,0 @@ -# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh --R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common --I gen-src --Q gen-src MetaCoq.Template --R theories MetaCoq.Template -META.coq-metacoq-template-ocaml --I . - -# Generated Code by `ls -1 gen-src/*.ml gen-src/*.mli` in `template-coq/` after having compiled `Extraction.v` -gen-src/all_Forall.ml -gen-src/all_Forall.mli -gen-src/ascii.ml -gen-src/ascii.mli -gen-src/ast0.ml -gen-src/ast0.mli -gen-src/astUtils.ml -gen-src/astUtils.mli -gen-src/ast_denoter.ml -gen-src/ast_quoter.ml -gen-src/basicAst.ml -gen-src/basicAst.mli -gen-src/basics.ml -gen-src/basics.mli -gen-src/binInt.ml -gen-src/binInt.mli -gen-src/binNat.ml -gen-src/binNat.mli -gen-src/binNums.ml -gen-src/binNums.mli -gen-src/binPos.ml -gen-src/binPos.mli -gen-src/binPosDef.ml -gen-src/binPosDef.mli -gen-src/decidableClass.mli -gen-src/decidableClass.ml -gen-src/bool.ml -gen-src/bool.mli -gen-src/byte.ml -gen-src/byte.mli -gen-src/byte0.ml -gen-src/byte0.mli -gen-src/byteCompare.ml -gen-src/byteCompare.mli -gen-src/byteCompareSpec.ml -gen-src/byteCompareSpec.mli -gen-src/bytestring.ml -gen-src/bytestring.mli -gen-src/cRelationClasses.ml -gen-src/cRelationClasses.mli -gen-src/caml_byte.ml -gen-src/caml_byte.mli -gen-src/caml_bytestring.ml -gen-src/caml_nat.ml -gen-src/caml_nat.mli -gen-src/carryType.ml -gen-src/carryType.mli -gen-src/classes0.ml -gen-src/classes0.mli -gen-src/common0.ml -gen-src/common0.mli -gen-src/compare_dec.ml -gen-src/compare_dec.mli -gen-src/config0.ml -gen-src/config0.mli -gen-src/coreTactics.ml -gen-src/coreTactics.mli -gen-src/datatypes.ml -gen-src/datatypes.mli -gen-src/decidableType.ml -gen-src/decidableType.mli -gen-src/decimal.ml -gen-src/decimal.mli -gen-src/denoter.ml -gen-src/depElim.ml -gen-src/depElim.mli -gen-src/envMap.ml -gen-src/envMap.mli -gen-src/environment.ml -gen-src/environment.mli -gen-src/environmentTyping.ml -gen-src/environmentTyping.mli -gen-src/eqDec.ml -gen-src/eqDec.mli -gen-src/eqDecInstances.ml -gen-src/eqDecInstances.mli -gen-src/eqdepFacts.ml -gen-src/eqdepFacts.mli -gen-src/equalities.ml -gen-src/equalities.mli -gen-src/extractable.ml -gen-src/extractable.mli -gen-src/fMapAVL.ml -gen-src/fMapAVL.mli -gen-src/fMapFacts.ml -gen-src/fMapFacts.mli -gen-src/fMapInterface.ml -gen-src/fMapInterface.mli -gen-src/fMapList.ml -gen-src/fMapList.mli -gen-src/floatClass.ml -gen-src/floatClass.mli -gen-src/floatOps.ml -gen-src/floatOps.mli -gen-src/hexadecimal.ml -gen-src/hexadecimal.mli -# gen-src/hexadecimalString.ml -# gen-src/hexadecimalString.mli -gen-src/induction0.ml -gen-src/induction0.mli -gen-src/init.ml -gen-src/init.mli -gen-src/int0.ml -gen-src/int0.mli -gen-src/kernames.ml -gen-src/kernames.mli -gen-src/liftSubst.ml -gen-src/liftSubst.mli -gen-src/list0.ml -gen-src/list0.mli -gen-src/logic0.ml -gen-src/logic0.mli -gen-src/logic1.ml -gen-src/logic1.mli -gen-src/logic2.ml -gen-src/logic2.mli -gen-src/mCCompare.ml -gen-src/mCCompare.mli -gen-src/mCFSets.ml -gen-src/mCFSets.mli -gen-src/mCList.ml -gen-src/mCList.mli -gen-src/mCMSets.ml -gen-src/mCMSets.mli -gen-src/mCOption.ml -gen-src/mCOption.mli -gen-src/mCPrelude.ml -gen-src/mCPrelude.mli -gen-src/mCProd.ml -gen-src/mCProd.mli -gen-src/mCReflect.ml -gen-src/mCReflect.mli -gen-src/mCRelations.ml -gen-src/mCRelations.mli -gen-src/mCString.ml -gen-src/mCString.mli -gen-src/sint63.mli -gen-src/sint63.ml -gen-src/show.mli -gen-src/show.ml -# gen-src/mCUint63.ml -# gen-src/mCUint63.mli -gen-src/mCUtils.ml -gen-src/mCUtils.mli -gen-src/mSetAVL.ml -gen-src/mSetAVL.mli -gen-src/mSetDecide.ml -gen-src/mSetDecide.mli -gen-src/mSetFacts.ml -gen-src/mSetFacts.mli -gen-src/mSetInterface.ml -gen-src/mSetInterface.mli -gen-src/mSetList.ml -gen-src/mSetList.mli -gen-src/mSetProperties.ml -gen-src/mSetProperties.mli -gen-src/monad_utils.ml -gen-src/monad_utils.mli -gen-src/nat0.ml -gen-src/nat0.mli -gen-src/noConfusion.ml -gen-src/noConfusion.mli -gen-src/number.ml -gen-src/number.mli -gen-src/orderedType0.ml -gen-src/orderedType0.mli -gen-src/orderedTypeAlt.ml -gen-src/orderedTypeAlt.mli -gen-src/orders.ml -gen-src/orders.mli -gen-src/ordersAlt.ml -gen-src/ordersAlt.mli -gen-src/ordersFacts.ml -gen-src/ordersFacts.mli -gen-src/ordersLists.ml -gen-src/ordersLists.mli -gen-src/ordersTac.ml -gen-src/ordersTac.mli -gen-src/peanoNat.ml -gen-src/peanoNat.mli -gen-src/plugin_core.ml -gen-src/plugin_core.mli -gen-src/pretty.ml -gen-src/pretty.mli -gen-src/primFloat.ml -gen-src/primFloat.mli -gen-src/primInt63.ml -gen-src/primInt63.mli -gen-src/primitive.ml -gen-src/primitive.mli -gen-src/quoter.ml -gen-src/reflect.ml -gen-src/reflect.mli -gen-src/reflectEq.ml -gen-src/reflectEq.mli -gen-src/reification.ml -gen-src/relation.ml -gen-src/relation.mli -gen-src/run_extractable.ml -gen-src/run_extractable.mli -gen-src/signature.ml -gen-src/signature.mli -gen-src/specFloat.ml -gen-src/specFloat.mli -gen-src/specif.ml -gen-src/specif.mli -gen-src/string0.ml -gen-src/string0.mli -gen-src/sumbool.ml -gen-src/sumbool.mli -gen-src/templateEnvMap.ml -gen-src/templateEnvMap.mli -gen-src/templateProgram.ml -gen-src/templateProgram.mli -gen-src/termEquality.ml -gen-src/termEquality.mli -gen-src/tm_util.ml -gen-src/transform.ml -gen-src/transform.mli -gen-src/typing0.ml -gen-src/typing0.mli -gen-src/uint0.ml -gen-src/uint0.mli -gen-src/universes0.ml -gen-src/universes0.mli -gen-src/wf.ml -gen-src/wf.mli -gen-src/zArith_dec.ml -gen-src/zArith_dec.mli -gen-src/zbool.ml -gen-src/zbool.mli -gen-src/zeven.ml -gen-src/zeven.mli -gen-src/zpower.ml -gen-src/zpower.mli - -gen-src/metacoq_template_plugin.mlpack - -theories/ExtractableLoader.v diff --git a/template-coq/_TemplateCoqProject b/template-coq/_TemplateCoqProject deleted file mode 100644 index 05f7e2517..000000000 --- a/template-coq/_TemplateCoqProject +++ /dev/null @@ -1,32 +0,0 @@ -# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh --R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common --I src --Q src MetaCoq.Template --R theories MetaCoq.Template -META.coq-metacoq-template-coq --I . - -# the MetaCoq plugin -src/tm_util.ml - -src/reification.ml -src/quoter.ml -src/denoter.ml -src/constr_reification.ml -src/constr_quoter.ml -src/constr_denoter.ml - -src/g_template_coq.mlg -src/template_coq.mlpack -src/template_monad.mli -src/template_monad.ml -src/run_template_monad.mli -src/run_template_monad.ml -src/plugin_core.mli -src/plugin_core.ml - -theories/Loader.v -theories/All.v - -# A checker of well-formedness in MetaCoq and Coq -theories/TemplateCheckWf.v