diff --git a/.gitignore b/.gitignore index c8c47c154bddd77dfc4cfc4ec6762757169b4136..1eb8cb496a914435d7a85a589a6700ce0bd1f0b4 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,7 @@ /remake.exe /src/gappatac.ml +/src/Gappa_tactic_loader.v *.o *.vo diff --git a/Remakefile.in b/Remakefile.in index 17ab8a3a4d637062c45c148815823de4951fb8a1..81533d2a4865f928218764a691c6c5e1eeb2bc1f 100644 --- a/Remakefile.in +++ b/Remakefile.in @@ -18,6 +18,7 @@ FILES = \ Gappa_round_def.v \ Gappa_round.v \ Gappa_tactic.v \ + Gappa_tactic_loader.v \ Gappa_tree.v \ Gappa_user.v @@ -39,7 +40,7 @@ configure config.status: configure.in ./config.status --recheck %.vo: %.v - @COQDEP@ -R src Gappa -I src $< | @REMAKE@ -r $@ + @COQDEP@ @COQDEPMETA@ -R src Gappa -I src $< | @REMAKE@ -r $@ @COQC@ @COQEXTRAFLAGS@ -R src Gappa -I src $< COQPKGS = clib engine kernel interp lib library parsing pretyping printing proofs tactics toplevel vernac plugins.ltac @@ -48,6 +49,9 @@ PACKAGES = $(addprefix -package @COQROOT@., $(COQPKGS)) -package @BIGINTPKG@ src/gappatac.ml: src/gappatac.c @CPP@ -DCOQVERSION=@COQVERSION@ $< -o $@ +src/Gappa_tactic_loader.v: src/Gappa_tactic_loader.c + @CPP@ -DCOQVERSION=@COQVERSION@ -P $< -o $@ + src/gappatac.cmo: src/gappatac.ml @OCAMLFIND@ ocamlc -rectypes -thread $(PACKAGES) -c $< -o $@ @@ -56,8 +60,8 @@ src/gappatac.cmxs: src/gappatac.ml MLTARGETS = $(addprefix src/, @TACTIC_TARGETS@) -src/Gappa_tactic.vo: src/Gappa_tactic.v $(MLTARGETS) - @COQDEP@ -R src Gappa -I src $< | @REMAKE@ -r $@ +src/Gappa_tactic.vo: src/Gappa_tactic.v src/Gappa_tactic_loader.v $(MLTARGETS) + @COQDEP@ @COQDEPMETA@ -R src Gappa -I src $< | @REMAKE@ -r $@ @COQC@ @COQEXTRAFLAGS@ @TACTIC_PARAM@ -R src Gappa -I src $< src/clean: @@ -99,8 +103,13 @@ testsuite/clean: install: dir="${DESTDIR}@COQUSERCONTRIB@/Gappa" mkdir -p $dir - cp $(OBJS) $(MLTARGETS) $dir + cp $(OBJS) $dir ( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "$dir/{}" \; ) + dir="${DESTDIR}@COQGAPPALIB@/" + mkdir -p $dir + cp $(MLTARGETS) $dir + cat src/META.coq-gappa | grep -v 'directory *=' > $dir/META + EXTRA_DIST = \ configure diff --git a/configure.in b/configure.in index 011d515f618d865fd6bf294e9bc6db4927ac5033..90241fe04ddb119924acfd84da79c4fbe1cba1d0 100644 --- a/configure.in +++ b/configure.in @@ -34,6 +34,11 @@ AX_VERSION_GE([$COQVERSION], [81400], [ COQROOT=coq ]) AC_SUBST(COQROOT) +AX_VERSION_GE([$COQVERSION], [81600], + [ COQDEPMETA="-m src/META.coq-gappa" ], + [ COQDEPMETA= ]) +AC_SUBST(COQDEPMETA) + AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]]) AC_MSG_CHECKING([for coqdep]) if test ! "$COQDEP"; then COQDEP=`which ${COQBIN}coqdep`; fi @@ -70,6 +75,11 @@ if test -z "$COQUSERCONTRIB"; then COQUSERCONTRIB="$COQLIB/user-contrib" fi +AX_VERSION_GE([$COQVERSION], [81600], + [ COQGAPPALIB=$COQLIB/../coq-gappa ], + [ COQGAPPALIB=$COQUSERCONTRIB/Gappa ]) +AC_SUBST(COQGAPPALIB) + AC_ARG_ENABLE([tactic], AS_HELP_STRING([--disable-tactic], [do not compile a "gappa" tactic]), [if test "$enable_tactic" = "no"; then native_tactic=no ; byte_tactic=no ; fi], []) diff --git a/src/Gappa_tactic.v b/src/Gappa_tactic.v index 04366a0a9fc8fb7b55ee0fa71304eae5d4cd3d1b..f74b9d54274f5a1a04679bd8dd15fc302756f988 100644 --- a/src/Gappa_tactic.v +++ b/src/Gappa_tactic.v @@ -1292,7 +1292,7 @@ End Gappa_Private. Import Gappa_Private. -Declare ML Module "gappatac". +Require Export Gappa_tactic_loader. Ltac gappa_prepare := intros ; fold rndNE rndNA in * ; diff --git a/src/Gappa_tactic_loader.c b/src/Gappa_tactic_loader.c new file mode 100644 index 0000000000000000000000000000000000000000..083aefadfb1e7a999e3d39dba00a8981e02667d1 --- /dev/null +++ b/src/Gappa_tactic_loader.c @@ -0,0 +1,5 @@ +#if COQVERSION >= 81600 +Declare ML Module "coq-gappa.tactic". +#else +Declare ML Module "gappatac". +#endif diff --git a/src/META.coq-gappa b/src/META.coq-gappa new file mode 100644 index 0000000000000000000000000000000000000000..7cdf7dc771351ff036f32b967b39a8eb693c96b4 --- /dev/null +++ b/src/META.coq-gappa @@ -0,0 +1,10 @@ +package "tactic" ( + directory = "." + description = "Coq Gappa" + requires = "coq-core.plugins.ltac" + archive(byte) = "gappatac.cma" + archive(native) = "gappatac.cmxa" + plugin(byte) = "gappatac.cma" + plugin(native) = "gappatac.cmxs" +) +directory = "." \ No newline at end of file diff --git a/src/gappatac.c b/src/gappatac.c index 5f2ebf9b09bd80c65482a13763809feb0e1bae4c..0406a83aea5e005a4505cbf5a276a1783e791ead 100644 --- a/src/gappatac.c +++ b/src/gappatac.c @@ -129,7 +129,12 @@ let constr_of_global f = Lazy.force f #endif +#if COQVERSION >= 81600 +let __coq_plugin_name = "coq-gappa.tactic" +#else let __coq_plugin_name = "gappatac" +#endif + let _ = Mltop.add_known_module __coq_plugin_name let debug = ref false