adapt to coq/coq#15220
I'd like to do something like
but I could not do it in remake, help is appreciated. I suspect the current code does not work well on cygwin.
Merge request reports
Activity
You can write arbitrary shell code inside rules. Just export
OCAMLPATHthere. But why do you need to do that? This seems awful. If it is to accommodate Findlib, couldn't you just callFindlib.init ~env_ocamlpath:"whatever -I directory passed on the command line"?Also, there is just no way I will ever accept a commit that transforms a
.vfile into a.cfile and adds preprocessing directives to it. How am I even supposed to interactively edit it now?
FTR dune sets OCAMLPATH to include the installation path of the project. I do something similar in coq_makefile with an export (like the code I pointed you to). Can I do a Remakefile-wide export?
Edited by TASSI EnricoPlease tell me if this is better.
Cannot you just name the plugin
coq-gappa.tactic? Or did earlier versions of Coq not support dots in plugin names?Can I do a Remakefile-wide export?
No.
OCAMLPATH points to a place where META files can be found
Where do you intend to install
META.coq-gappa?By the way, do not modify the content of
$COQDEPinconfigure.in. Just change@COQDEP@into@COQDEP@ @COQDEPMETA@insideRemakefile.in.The META file should go to
.../lib/coq-gappa/META(I forgot to fix that)And where are
gappatac.cm{o,xs}supposed to be installed? In that same directory?If so, you could just put the
METAfile in thesrcdirectory, then Coq would use-Ito callFindlib.initaccordingly, and build scripts would never need to mess withOCAMLPATH.-
Your idea makes sense, but in a few cases I have 1 package with multiple plugins in different directories, not sure I can have multiple META.package in scope (even if they define different package.library).
I'll give it a try, but I can't promise anything. In the meanwhile please bear with OCAMLPATH.
In the meanwhile, this commit should fix the installation
mentioned in commit 8a824e7c
