Add target to update template-coq _PluginProject.in

template-coq/Makefile

@@ -72,3 +72,28 @@ mrproper:
 
 cleanplugin: Makefile.plugin
 	make -f Makefile.plugin clean
+
+PLUGIN_PROJECT_BLACKLIST := \
+	carryType \
+	coreTactics \
+	depElim \
+	floatClass \
+	init \
+	mCUint63 \
+	noConfusion \
+	wf \
+	#
+
+space := $(subst ,, )
+
+PLUGIN_PROJECT_BLACKLIST_SED:=\($(subst $(space),\|,$(PLUGIN_PROJECT_BLACKLIST))\)\.\(ml\|mli\)
+
+.PHONY: update-_PluginProject.in
+update-_PluginProject.in:
+	@echo 'WARNING: This target only works correctly when gen-src has been populated from making Extraction.vo and contains no outdated .ml{,i} files'
+	contents="$$(cat _PluginProject.in | grep -v '^gen-src/.*\.\(mli\|ml\)$$')"; \
+	line="$$(printf "%s\n" "$${contents}" | grep -n "^# Generated" | head -1 | cut -d: -f1)"; \
+	{ printf "%s\n" "$${contents}" | head -n$${line}; \
+	  ls -1 gen-src/*.ml gen-src/*.mli | env LC_COLLATE=C sort | sed 's,^\(gen-src/$(PLUGIN_PROJECT_BLACKLIST_SED)\)$$,# \1,g'; \
+	  printf "%s\n" "$${contents}" | tail -n+$$((line+1)); \
+	} > _PluginProject.in

template-coq/_PluginProject

@@ -6,132 +6,143 @@
 META.coq-metacoq-template-ocaml
 -I .
 
-# Generated Code by `ls -1 *.ml *.mli` in `template-coq/gen-src` after having compiled `Extraction.v`
-gen-src/signature.mli
-gen-src/signature.ml
-gen-src/classes0.mli
-gen-src/classes0.ml
-gen-src/eqDec.mli
-gen-src/eqDec.ml
+# 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/caml_nat.mli
-gen-src/caml_nat.ml
 gen-src/ast0.ml
 gen-src/ast0.mli
-gen-src/ast_denoter.ml
-gen-src/ast_quoter.ml
-gen-src/primitive.mli
-gen-src/primitive.ml
 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/binNums.mli
-gen-src/binNums.ml
 gen-src/binInt.ml
 gen-src/binInt.mli
 gen-src/binNat.ml
 gen-src/binNat.mli
-gen-src/binPosDef.ml
-gen-src/binPosDef.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/bool.ml
 gen-src/bool.mli
-gen-src/monad_utils.mli
-gen-src/monad_utils.ml
+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/cRelationClasses.ml
-gen-src/cRelationClasses.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/decimalString.ml
+gen-src/decimalString.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.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/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/induction.ml
-#gen-src/induction.mli
-#gen-src/mCUint63.mli
-#gen-src/mCUint63.ml
-gen-src/primInt63.ml
-gen-src/primInt63.mli
-gen-src/uint0.ml
-gen-src/uint0.mli
+gen-src/hexadecimalString.ml
+gen-src/hexadecimalString.mli
+gen-src/induction.ml
+gen-src/induction.mli
+# gen-src/init.ml
+# gen-src/init.mli
 gen-src/int0.ml
 gen-src/int0.mli
-gen-src/sumbool.mli
-gen-src/sumbool.ml
-gen-src/zeven.mli
-gen-src/zeven.ml
-gen-src/zArith_dec.mli
-gen-src/zArith_dec.ml
-gen-src/zbool.mli
-gen-src/zbool.ml
-gen-src/zpower.mli
-gen-src/zpower.ml
-gen-src/specFloat.mli
-gen-src/specFloat.ml
-gen-src/floatOps.mli
-gen-src/floatOps.ml
-# gen-src/float64.mli
-# gen-src/float64.ml
+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.mli
 gen-src/logic1.ml
-gen-src/logic2.mli
+gen-src/logic1.mli
 gen-src/logic2.ml
-gen-src/relation.mli
-gen-src/relation.ml
-gen-src/mCProd.mli
-gen-src/mCProd.ml
-gen-src/mCPrelude.mli
-gen-src/mCPrelude.ml
+gen-src/logic2.mli
 gen-src/mCCompare.ml
 gen-src/mCCompare.mli
-gen-src/reflectEq.mli
-gen-src/reflectEq.ml
 gen-src/mCList.ml
 gen-src/mCList.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/mCReflect.mli
-gen-src/mCReflect.ml
-gen-src/primFloat.mli
-gen-src/primFloat.ml
-gen-src/hexadecimalString.mli
-gen-src/hexadecimalString.ml
-gen-src/decimalString.mli
-gen-src/decimalString.ml
 gen-src/mCString.ml
 gen-src/mCString.mli
+# 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
@@ -140,86 +151,85 @@ gen-src/mSetInterface.ml
 gen-src/mSetInterface.mli
 gen-src/mSetList.ml
 gen-src/mSetList.mli
-gen-src/mSetAVL.ml
-gen-src/mSetAVL.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/ordersFacts.ml
 gen-src/ordersFacts.mli
 gen-src/ordersLists.ml
 gen-src/ordersLists.mli
-gen-src/orders.ml
-gen-src/orders.mli
 gen-src/ordersTac.ml
 gen-src/ordersTac.mli
-gen-src/orderedType0.mli
-gen-src/orderedType0.ml
-gen-src/orderedTypeAlt.mli
-gen-src/orderedTypeAlt.ml
-gen-src/decidableType.mli
-gen-src/decidableType.ml
-gen-src/fMapList.mli
-gen-src/fMapList.ml
-gen-src/fMapInterface.mli
-gen-src/fMapInterface.ml
-gen-src/fMapAVL.mli
-gen-src/fMapAVL.ml
-gen-src/fMapFacts.mli
-gen-src/fMapFacts.ml
 gen-src/peanoNat.ml
 gen-src/peanoNat.mli
 gen-src/plugin_core.ml
 gen-src/plugin_core.mli
-gen-src/induction.mli
-gen-src/induction.ml
-gen-src/eqDecInstances.mli
-gen-src/eqDecInstances.ml
-gen-src/reflect.mli
-gen-src/reflect.ml
 gen-src/pretty.ml
 gen-src/pretty.mli
-gen-src/reification.ml
+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/byte0.mli
-gen-src/byte0.ml
-gen-src/byte.mli
-gen-src/byte.ml
-gen-src/caml_byte.mli
-gen-src/caml_byte.ml
-gen-src/byteCompare.mli
-gen-src/byteCompare.ml
-gen-src/byteCompareSpec.mli
-gen-src/byteCompareSpec.ml
-gen-src/bytestring.mli
-gen-src/bytestring.ml
-gen-src/caml_bytestring.ml
+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/kernames.mli
-gen-src/kernames.ml
-gen-src/universes0.ml
-gen-src/universes0.mli
-gen-src/transform.mli
 gen-src/transform.ml
-gen-src/termEquality.mli
-gen-src/termEquality.ml
-gen-src/envMap.mli
-gen-src/envMap.ml
-gen-src/templateEnvMap.mli
-gen-src/templateEnvMap.ml
-gen-src/typing0.mli
+gen-src/transform.mli
 gen-src/typing0.ml
-gen-src/templateProgram.mli
-gen-src/templateProgram.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