Port Fiat to coqpp

[ppedrot]

The Fiat repository should be ported to the coqpp tool for Coq master, by turning the ml4 files into mlg and adapting the code correspondingly. While the code adaptation is trivial, Fiat seems to do black magic in its makefile to pick the right file depending on the Coq version. I don't really understand that part enough to fix it though, hence this bug report.

Regarding the port, the following diff should be enough:

--- a/src/Common/Tactics/hint_db_extra_plugin.ml4.master
+++ b/src/Common/Tactics/hint_db_extra_plugin.mlg.master
@@ -1,16 +1,20 @@
+{
+
 open Hint_db_extra_tactics
 open Stdarg
 open Ltac_plugin
 open Tacarg

+}
+
 DECLARE PLUGIN "hint_db_extra_plugin"

 TACTIC EXTEND foreach_db
   | [ "foreach" "[" ne_preident_list(l) "]" "run" tactic(k) ]  ->
-     [ WITH_DB.with_hint_db l k ]
+     { WITH_DB.with_hint_db l k }
        END

 TACTIC EXTEND addto_db
   | [ "add" constr(name) "to" ne_preident_list(l) ]  ->
-     [ WITH_DB.add_resolve_to_db (Hints.IsConstr (name, Univ.ContextSet.empty)) l]
-       END;;
+     { WITH_DB.add_resolve_to_db (Hints.IsConstr (name, Univ.ContextSet.empty)) l }
+       END

--- a/src/Common/Tactics/transparent_abstract_plugin.ml4.master
+++ b/src/Common/Tactics/transparent_abstract_plugin.mlg.master
@@ -1,21 +1,25 @@
+{
+
 open Transparent_abstract_tactics
 open Stdarg
 open Ltac_plugin
 open Tacarg

+}
+
 DECLARE PLUGIN "transparent_abstract_plugin"

 TACTIC EXTEND transparentabstract
 | [ "cache" tactic(tac) "as" ident(name)]
--> [ TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) ]
+-> { TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) }
 END

 TACTIC EXTEND abstracttermas
 | [ "cache_term" constr(term) "as" ident(name) "run" tactic(tacK)]  ->
-[ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK  ]
+{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK  }
 END

 TACTIC EXTEND abstractterm
 | [ "cache_term" constr(term) "run" tactic(tacK) ]  ->
-[ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK ]
-END;;
+{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK }
+END

[JasonGross]

That change is not sufficient, as it breaks parallel compilation, because _CoqProject does not know about the .mlg files. Is there any _CoqProject that is compatible with both master and non-master? We rely on _CoqProject being the same across all versions.

[ppedrot]

Unluckily I don't think this can be fixed without backporting a few patches to those Coq versions. Can't you really dispatch _CoqProject depending on the version of Coq? It's only a matter of calling a sed script...

[JasonGross]

_CoqProject is version-controlled, but I'll see what I can do.

[JasonGross]

@ppedrot How new a master do I need to do this? https://github.com/coq/coq/commits/71296e6e91de5b3fea08ef4b34426a02304f00b8 does not work, as coq_makefile -f _CoqProject errors with "Unknown option src/Common/Tactics/hint_db_extra_plugin.mlg"