diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Makefile.oug | 74 | ||||
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 46 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-coquelicot.sh | 21 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-crypto.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-flocq.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 24 | ||||
| -rwxr-xr-x | dev/ci/ci-math-classes.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-math-comp.sh | 10 | ||||
| -rwxr-xr-x | dev/ci/ci-metacoq.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-tlc.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 15 | ||||
| -rw-r--r-- | dev/core.dbg | 1 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 18 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 4 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
19 files changed, 113 insertions, 138 deletions
diff --git a/dev/Makefile.oug b/dev/Makefile.oug deleted file mode 100644 index ee69ea80df..0000000000 --- a/dev/Makefile.oug +++ /dev/null @@ -1,74 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### - - -#### Source Code Analysis via Oug #### -#### Cf http://home.gna.org/oug #### - - -# To be used from top dir : make -f dev/Makefile.oug ... - -include Makefile.build - -# Oug location: in the path by default, native version - -OUG:=oug.x - -# NB: coq should have been compiled with the same ocaml version as oug - -# NOTA: it seems we obtain more useless elements reported when _not_ -# providing the .mli files, and also when giving a precise start point. -# TO BE INVESTIGATED - -ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d)))) -local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1))) -mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i)) - -# Analysis of coqtop, without plugins - -COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA)) -COREMLI:=$(call mli_of_ml,$(COREML)) - -core.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) - -core.useless: core.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -core_intf.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI) - -core_intf.useless: core_intf.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -# Analysis of coqchk, considering only files in the checker/ subdir - -CHECKERML:=$(call local_ml_of_cma,checker/check.cma) -CHECKERMLI:=$(call mli_of_ml,$(CHECKERML)) - -## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS -MYCHKINCL:=$(MLINCLUDES) -I checker - -checker.oug: - $(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI) - -checker.useless: checker.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@ - -# Analysis of extraction - -EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA)) -EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI)) - -extraction.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI) - -extraction.useless: extraction.oug - $(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@ - -# More to come ...
\ No newline at end of file diff --git a/dev/base_include b/dev/base_include index 0abcefc38e..242405ae29 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,7 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a6601e045..412da626fd 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,5 +2,51 @@ set -xe +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN=`pwd`/bin/ export PATH=`pwd`/bin:$PATH + ls `pwd`/bin + +# Maybe we should just use Ruby... +mathcomp_CI_BRANCH=master +mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git + +# git_checkout branch +git_checkout() +{ + local _BRANCH=${1} + local _URL=${2} + local _DEST=${3} + + echo "Checking out ${_DEST}" + git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} + ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) +} + +checkout_mathcomp() +{ + git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + checkout_mathcomp math-comp + ( cd math-comp/mathcomp && \ + sed -i.bak '/ssrtest/d' Make && \ + sed -i.bak '/odd_order/d' Make && \ + sed -i.bak '/all\/all.v/d' Make && \ + sed -i.bak '/character/d' Make && \ + sed -i.bak '/real_closed/d' Make && \ + sed -i.bak '/solvable/d' Make && \ + sed -i.bak '/field/d' Make && \ + sed -i.bak '/fingroup/d' Make && \ + sed -i.bak '/algebra/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + + echo -en 'travis_fold:end:ssr.install\\r' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4023c9165..ec09389f8e 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +CompCert_CI_BRANCH=master +CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git + opam install -j ${NJOBS} -y menhir -git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert # Patch to avoid the upper version limit ( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 4a23e51be6..94bd5e468f 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -4,26 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup coquelicot -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot ( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c594f83603..c669195ddd 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -4,9 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git +git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto ( cd fiat-crypto && make -j ${NJOBS} ) - -# ( cd corn && make -j ${NJOBS} ) - diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index b9cf649a1a..345924e40a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -4,6 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq ( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7b5811dc4a..ce870e52b5 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,6 +7,10 @@ source ${ci_dir}/ci-common.sh GeoCoq_CI_BRANCH=master GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git -git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq -( cd GeoCoq && ./configure.sh && make -j ${NJOBS} ) +( cd GeoCoq && \ + ./configure.sh && \ + sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + coq_makefile -f Make -o Makefile && \ + make -j ${NJOBS} ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 8f82ba9f21..0c07564c02 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git +git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index e97e2c19e3..c21af976f4 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -4,32 +4,14 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Refactor into install-ssreflect -git clone --depth 1 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup stdpp -git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git +git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp ( cd coq-stdpp && make -j ${NJOBS} && make install ) # Setup Iris -git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git +git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq ( cd iris-coq && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 9127c18951..4450dc0710 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -4,9 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git +git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes ( cd math-classes && make -j ${NJOBS} && make install ) -git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git +git_checkout v8.6 https://github.com/c-corn/corn.git corn ( cd corn && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index b833792419..2eb150cb52 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git +checkout_mathcomp math-comp # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) +( cd math-comp/mathcomp && \ + sed -i.bak '/PFsection/d' Make && \ + sed -i.bak '/stripped_odd_order_theorem/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 9a9bd3648b..91a33695b0 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -6,11 +6,11 @@ source ${ci_dir}/ci-common.sh # MetaCoq + UniCoq -git clone --depth 1 https://github.com/unicoq/unicoq.git +git_checkout master https://github.com/unicoq/unicoq.git unicoq ( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git +git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq ( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 2161a11461..b946324924 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone https://gforge.inria.fr/git/tlc/tlc.git +git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc ( cd tlc && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 0000000000..15e619acbb --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_BRANCH=master +UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath + +( cd UniMath && \ + sed -i.bak '/Folds/d' Makefile && \ + sed -i.bak '/HomologicalAlgebra/d' Makefile && \ + make -j ${NJOBS} BUILD_COQ=no ) + diff --git a/dev/core.dbg b/dev/core.dbg index 38b9b29463..698db63d23 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -12,6 +12,7 @@ load_printer proofs.cma load_printer parsing.cma load_printer printing.cma load_printer tactics.cma +load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..8d2d055908 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,24 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The folder itself has been turned into a plugin. This does not change much, +but because it is a packed plugin, it may wreak havoc for third-party plugins +depending on any module defined in the ltac/ directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +an error of the form: + +Error: while loading myplugin.cmxs, no implementation available for Foo. + +In particular, most EXTEND macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement "open Ltac_plugin" +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not +work for EXTEND macros though. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 46caca8d6f..3850c05fd9 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ - -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ @@ -32,6 +32,6 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ "$@" diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fcad88202..dc354b130b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -234,7 +234,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) |