diff options
Diffstat (limited to 'dev')
33 files changed, 576 insertions, 460 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_db b/dev/base_db index b540aed6ca..e18ac534ac 100644 --- a/dev/base_db +++ b/dev/base_db @@ -1,6 +1,6 @@ -load_printer "gramlib.cma" -load_printer "top_printers.cmo" -install_printer Top_printers.prid -install_printer Top_printers.prsp -install_printer Top_printers.print_pure_constr +source core.dbg +load_printer top_printers.cmo +install_printer Top_printers.ppid +install_printer Top_printers.ppsp +install_printer Top_printers.ppconstr diff --git a/dev/base_include b/dev/base_include index b09b6df2de..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 Pcoq.Tactic.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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 0000000000..241ec35861 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,103 @@ +#!/usr/bin/env bash + +# This is the basic overlay set for repositories in the CI. + +# Maybe we should just use Ruby to have real objects... + +######################################################################## +# MathComp +######################################################################## +: ${mathcomp_CI_BRANCH:=master} +: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} + +######################################################################## +# UniMath +######################################################################## +: ${UniMath_CI_BRANCH:=master} +: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} + +######################################################################## +# Unicoq + Metacoq +######################################################################## +: ${unicoq_CI_BRANCH:=master} +: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} + +: ${metacoq_CI_BRANCH:=master} +: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} + +######################################################################## +# Mathclasses + Corn +######################################################################## +: ${math_classes_CI_BRANCH:=v8.6} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} + +: ${Corn_CI_BRANCH:=v8.6} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} + +######################################################################## +# Iris +######################################################################## +: ${stdpp_CI_BRANCH:=master} +: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} + +: ${Iris_CI_BRANCH:=master} +: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} + +######################################################################## +# HoTT +######################################################################## +: ${HoTT_CI_BRANCH:=mz-8.7} +: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} + +######################################################################## +# GeoCoq +######################################################################## +: ${GeoCoq_CI_BRANCH:=master} +: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} + +######################################################################## +# Flocq +######################################################################## +: ${Flocq_CI_BRANCH:=master} +: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${Coquelicot_CI_BRANCH:=master} +: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} + +######################################################################## +# CompCert +######################################################################## +: ${CompCert_CI_BRANCH:=master} +: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} + +######################################################################## +# fiat_parsers +######################################################################## +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} + +######################################################################## +# fiat_crypto +######################################################################## +: ${fiat_crypto_CI_BRANCH:=master} +: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} + +######################################################################## +# CoLoR +######################################################################## +: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} + +######################################################################## +# SF +######################################################################## +: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz} + +######################################################################## +# TLC +######################################################################## +: ${tlc_CI_BRANCH:=master} +: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} + diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 78ae7f02f9..3f0716511d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color +Color_CI_DIR=${CI_BUILD_DIR}/color -( cd color && make -j ${NJOBS} ) +svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} + +( cd ${Color_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 412da626fd..c94f150263 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -xe @@ -8,20 +8,30 @@ 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 +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci -# git_checkout branch +source ${ci_dir}/ci-user-overlay.sh +source ${ci_dir}/ci-basic-overlay.sh + +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +# git_checkout branch url dest will create a git repository +# in <dest> (if it does not exist already) and checkout the +# remote branch <branch> from <url> 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'`" ) + mkdir -p ${_DEST} + ( cd ${_DEST} && \ + if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch ${_URL} ${_BRANCH} && \ + git checkout FETCH_HEAD && \ + echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } checkout_mathcomp() @@ -34,8 +44,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp math-comp - ( cd math-comp/mathcomp && \ + checkout_mathcomp ${mathcomp_CI_DIR} + ( cd ${mathcomp_CI_DIR}/mathcomp && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ sed -i.bak '/all\/all.v/d' Make && \ diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index ec09389f8e..c78ffdc2c0 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,13 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -CompCert_CI_BRANCH=master -CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git +CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir -git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} # 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} ) +( cd ${CompCert_CI_DIR} && 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 94bd5e468f..40eff03b78 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot + install_ssreflect -# Setup coquelicot -git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot +git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} -( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 18d7561804..0e791ebbfd 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c669195ddd..93d39aab07 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto +fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto -( cd fiat-crypto && make -j ${NJOBS} ) +git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} + +( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 0000000000..c62aa1d859 --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} + +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 345924e40a..ec19bd9939 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq +Flocq_CI_DIR=${CI_BUILD_DIR}/flocq -( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} + +( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 29667b018a..4e5aa2687b 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,15 +1,13 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: replace by generic template -GeoCoq_CI_BRANCH=master -GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git +GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} -( cd GeoCoq && \ +( cd ${GeoCoq_CI_DIR} && \ ./configure.sh && \ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ sed -i.bak '/Elements\/Book_1\.v/d' Make && \ diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 0c07564c02..1bf6e9a872 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT +HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT -( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) +git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} + +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index c21af976f4..eb1d1be078 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,17 +1,22 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp + +Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq + install_ssreflect # Setup stdpp -git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp -( cd coq-stdpp && make -j ${NJOBS} && make install ) +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} + +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) # Setup Iris -git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq -( cd iris-coq && make -j ${NJOBS} ) +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} + +( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4450dc0710..beb75773b7 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,12 +1,20 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes -( cd math-classes && make -j ${NJOBS} && make install ) +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes -git_checkout v8.6 https://github.com/c-corn/corn.git corn -( cd corn && make -j ${NJOBS} ) +Corn_CI_DIR=${CI_BUILD_DIR}/corn +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 2eb150cb52..bb8188da4e 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,13 +1,15 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -checkout_mathcomp math-comp +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +checkout_mathcomp ${mathcomp_CI_DIR} # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ +( cd ${mathcomp_CI_DIR}/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 91a33695b0..e31691179e 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,16 +1,19 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# MetaCoq + UniCoq +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq +metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq -git_checkout master https://github.com/unicoq/unicoq.git unicoq +# Setup UniCoq -( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} -git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) +# Setup MetaCoq +git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} + +( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 5e41211f1a..7d23ccad97 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz +# XXX: Needs fixing to properly set the build directory. +wget ${sf_CI_TARURL} tar xvfz sf.tgz ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh new file mode 100755 index 0000000000..700105aed4 --- /dev/null +++ b/dev/ci/ci-template.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Template_CI_BRANCH=master +Template_CI_GITURL=https://github.com/Template/Template +Template_CI_DIR=${CI_BUILD_DIR}/Template + +git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} + +( cd ${Template_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index b946324924..ce26399378 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc +tlc_CI_DIR=${CI_BUILD_DIR}/tlc -( cd tlc && make -j ${NJOBS} ) +git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} + +( cd ${tlc_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 15e619acbb..175b82b5f9 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,13 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -UniMath_CI_BRANCH=master -UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git +UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath -git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} -( cd UniMath && \ +( cd ${UniMath_CI_DIR} && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ make -j ${NJOBS} BUILD_COQ=no ) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh new file mode 100644 index 0000000000..0285747432 --- /dev/null +++ b/dev/ci/ci-user-overlay.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash + +# Add user overlays here. You can use some logic to detect if you are +# in your travis branch and conditionally enable the overlay. + +# Some useful Travis variables: +# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables) +# +# - TRAVIS_BRANCH: For builds not triggered by a pull request this is +# the name of the branch currently being built; whereas for builds +# triggered by a pull request this is the name of the branch +# targeted by the pull request (in many cases this will be master). +# +# - TRAVIS_COMMIT: The commit that the current build is testing. +# +# - TRAVIS_PULL_REQUEST: The pull request number if the current job is +# a pull request, “false” if it’s not a pull request. +# +# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request, +# the name of the branch from which the PR originated. "" if the +# current job is a push build. + diff --git a/dev/core.dbg b/dev/core.dbg new file mode 100644 index 0000000000..f04e5c07b7 --- /dev/null +++ b/dev/core.dbg @@ -0,0 +1,19 @@ +source camlp4.dbg +load_printer threads.cma +load_printer str.cma +load_printer clib.cma +load_printer lib.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +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 +load_printer ltac_plugin.cmo @@ -1,4 +1,5 @@ -load_printer "printers.cma" +source core.dbg +load_printer top_printers.cmo install_printer Top_printers.ppfuture diff --git a/dev/doc/api.txt b/dev/doc/api.txt new file mode 100644 index 0000000000..5827257b53 --- /dev/null +++ b/dev/doc/api.txt @@ -0,0 +1,10 @@ +Recommendations in using the API: + +The type of terms: constr (see kernel/constr.ml and kernel/term.ml) + +- On type constr, the canonical equality on CIC (up to + alpha-conversion and cast removal) is Constr.equal +- The type constr is abstract, use mkRel, mkSort, etc. to build + elements in constr; use "kind_of_term" to analyze the head of a + constr; use destRel, destSort, etc. when the head constructor is + known diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 3de938d774..03742fb8ad 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,134 @@ ========================================= += CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = +========================================= + +* Ocaml * + +Coq is compiled with -safe-string enabled and requires plugins to do +the same. This means that code using `String` in an imperative way +will fail to compile now. They should switch to `Bytes.t` + +* ML API * + +We renamed the following functions: + + Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr + Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr + Printer.pr_var_list_decl -> Printer.pr_compacted_decl + Printer.pr_var_decl -> Printer.pr_named_decl + Nameops.lift_subscript -> Nameops.increment_subscript + +We removed the following functions: + + Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context + Namegen.to_avoid ... equivalent substitute is Names.Id.List.mem + +We renamed the following modules: + + Context.ListNamed -> Context.Compacted + +The following type aliases where removed + + Context.section_context ... it was just an alias for "Context.Named.t" which is still available + +The module Constrarg was merged into Stdarg. + +** Ltac API ** + +Many Ltac specific API has been moved in its own ltac/ folder. Amongst other +important things: + +- Pcoq.Tactic -> Pltac +- Constrarg.wit_tactic -> Tacarg.wit_tactic +- Constrarg.wit_ltac -> Tacarg.wit_ltac +- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument + instead +- Some printing functions were moved from Pptactic to Pputils +- A part of Tacexpr has been moved to Tactypes +- The TacFun tactic expression constructor now takes a `Name.t list` for the + variable list rather than an `Id.t option list`. + +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 + functions that used to carry a suffix `_loc`, such suffix has been + dropped. + +- `errorlabstrm` has been removed in favor of `user_err`. + +- The header parameter to `user_err` has been made optional. + +** Pretty printing ** + +Some functions have been removed, see pretty printing below for more +details. + +* Pretty Printing and XML protocol * + +The type std_cmdpps has been reworked and made the canonical "Coq rich +document type". This allows for a more uniform handling of printing +(specially in IDEs). The main consequences are: + + - Richpp has been confined to IDE use. Most of previous uses of the + `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API + has been updated. + + - The XML protocol will send a new message type of `pp`, which should + be rendered client-wise. + + - `Set Printing Width` is deprecated, now width is controlled + client-side. + + - `Pp_control` has removed. The new module `Topfmt` implements + console control for the toplevel. + + - The impure tag system in Pp has been removed. This also does away + with the printer signatures and functors. Now printers tag + unconditionally. + + - The following functions have been removed from `Pp`: + + val stras : int * string -> std_ppcmds + val tbrk : int * int -> std_ppcmds + val tab : unit -> std_ppcmds + val pifb : unit -> std_ppcmds + val comment : int -> std_ppcmds + val comments : ((int * int) * string) list ref + val eval_ppcmds : std_ppcmds -> std_ppcmds + val is_empty : std_ppcmds -> bool + val t : std_ppcmds -> std_ppcmds + val hb : int -> std_ppcmds + val vb : int -> std_ppcmds + val hvb : int -> std_ppcmds + val hovb : int -> std_ppcmds + val tb : unit -> std_ppcmds + val close : unit -> std_ppcmds + val tclose : unit -> std_ppcmds + val open_tag : Tag.t -> std_ppcmds + val close_tag : unit -> std_ppcmds + val msg_with : ... + + module Tag + +========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index f0df2fc371..79cde48849 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -51,8 +51,8 @@ Debugging from Caml debugger failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle of each of error* functions or anomaly* functions in lib/util.ml - - If "source db" fails, recompile printers.cma with - "make dev/printers.cma" and try again + - If "source db" fails, do a "make printers" and try again (it should build + top_printers.cmo and the core cma files). Global gprof-based profiling ============================ diff --git a/dev/doc/style.txt b/dev/doc/style.txt index 27695a09b1..2ee3dadd77 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,75 +1,142 @@ - -<< L'uniformité du style est plus importante que le style lui-même. >> -(Kernigan & Pike, The Practice of Programming) - -Mode Emacs -========== - Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - - avec le réglage suivant : (setq tuareg-in-indent 2) - -Types récursifs et filtrages -============================ - Une barre de séparation y compris sur le premier constructeur - -type t = - | A - | B of machin - -match expr with - | A -> ... - | B x -> ... - -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le -format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : - -type t = -| A -| B of machin - -match expr with -| A -> ... -| B x -> ... - -let f expr = match expr with -| A -> ... -| B x -> ... - -let f expr = function -| A -> ... -| B x -> ... - -Le deuxième cas est obtenu sous tuareg avec les réglages - - (setq tuareg-with-indent 0) - (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien - /// pour les let mais pas pour les let-in - -Conditionnelles -=============== - if condition then - premier-cas - else - deuxieme-cas - - Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. - - if condition then begin - instr1; - instr2 - end else begin - instr3; - instr4 - end - - Si la première branche lève une exception, évitez le else i.e. - - if condition then if condition then error "machin"; - error "machin" -----> suite +<< Style uniformity is more important than style itself >> + (Kernigan & Pike, The Practice of Programming) + +OCaml Style: +- Spacing and indentation + - indent your code (using tuareg default) + - no strong constraints in formatting "let in"; possible styles are: + "let x = ... in" + "let x = + ... in" + "let + x = ... + in" + - but: no extra indentation before a "in" coming on next line, + otherwise, it first shifts further and further on the right, + reducing the amount of space available; second, it is not robust to + insertion of a new "let" + - it is established usage to have space around "|" as in + "match c with + | [] | [a] -> ... + | a::b::l -> ..." + - in a one-line "match", it is preferred to have no "|" in front of + the first case (this saves spaces for the match to hold in the line) + - from about 8.2, the tendency is to use the following format which + limit excessive indentation while providing an interesting "block" aspect + type t = + | A + | B of machin + + let f expr = match expr with + | A -> ... + | B x -> ... + + let f expr = function + | A -> ... + | B x -> ... + - add spaces around = and == (make the code "breaths") + - the common usage is to write "let x,y = ... in ..." rather than + "let (x,y) = ... in ..." + - parenthesizing with either "(" and ")" or with "begin" and "end" is + common practice + - preferred layout for conditionals: + if condition then + premier-cas else - suite - - + deuxieme-cas + - in case of effects in branches, use "begin ... end" rather than + parentheses + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + - if the first branch raises an exception, avoid the "else", i.e.: + if condition then if condition then error "foo"; + error "foo" -----> bar + else + bar + - it is the usage not to use ;; to end OCaml sentences (however, + inserting ";;" can be useful for debugging syntax errors crossing + the boundary of functions) + - relevant options in tuareg: + (setq tuareg-in-indent 2) + (setq tuareg-with-indent 0) + (setq tuareg-function-indent 0) + (setq tuareg-let-always-indent nil) + +- Coding methodology + - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C), + Out_of_memory, Stack_overflow, etc. + at least, use "try with e when Errors.noncritical e -> ..." + (to be detailed, Pierre L. ?) + - do not abuse of fancy combinators: sometimes what a "let rec" loop + does is more readable and simpler to grasp than what a "fold" does + - do not break abstractions: if an internal property is hidden + behind an interface, do no rely on it in code which uses this + interface (e.g. do not use List.map thinking it is left-to-right, + use map_left) + - in particular, do not use "=" on abstract types: there is no + reason a priori that it is the intended equality on this type; use the + "equal" function normally provided with the abstract type + - avoid polymorphically typed "=" whose implementation is not + optimized in OCaml and which has moreover no reason to be the + intended implementation of the equality when it comes to be + instantiated on a particular type (e.g. use List.mem_f, + List.assoc_f, rather than List.mem, List.assoc, etc, unless it is + absolutely clear that "=" will implement the intended equality, and + with the right complexity) + - any new general-purpose enough combinator on list should be put in + cList.ml, on type option in cOpt.ml, etc. + - unless of a good reason not to so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breaths" (we + have large screen nowadays), "make your code easy to read and + to understand" + - document what is tricky, but do not overdocument, sometimes the + choice of names and the structuration of the code is a better + documentation than a long discourse; use of unicode in comments is + welcome if it can make comments more readable (then + "toggle-enable-multibyte-characters" can help when using the + debugger in emacs) + - all of initial "open File", or of small-scope File.(...), or + per-ident File.foo are common practices + +- Choice of variable names + - be consistent when naming from one function to another + - be consistent with the naming adopted in the functions from the + same file, or with the naming used elsewhere by similar functions + - use variable names which express meaning + - keep "cst" for constants and avoid it for constructors which is + otherwise a source of confusion + - for constructors, use "cstr" in type constructor (resp. "cstru" in + constructor puniverse); avoid "constr" for "constructor" which + could be think as the name of an arbitrary Constr.t + - for inductive types, use "ind" in the type inductive (resp "indu" + in inductive puniverse) + - for env, use "env" + - for evar_map, use "sigma", with tolerance into "evm" and "evd" + - for named_context or rel_context, use "ctxt" or "ctx" (or "sign") + - for formal/actual indices of inductive types: "realdecls", "realargs" + - for formal/actual parameters of inductive types: "paramdecls", "paramargs" + - for terms, use e.g. c, b, a, ... + - if a term is known to be a function: f, ... + - if a term is known to be a type: t, u, typ, ... + - for a declaration, use d or "decl" + - for errors, exceptions, use e + +- Common OCaml pitfalls + - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in + "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in + parentheses are needed around the "try" and the inner "match" + - even if stream are lazy, the Pp.(++) combinator is strict and + forces the evaluation of its arguments (use a "lazy" or a "fun () ->") + to make it lazy explicitly + - in "if ... then ... else ... ++ ...", the default parenthesizing + is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..." + - in "let myspecialfun = mygenericfun args", be sure that it does no + do side-effect; prefer otherwise "let mygenericfun arg = + mygenericfun args arg" to ensure that the function is evaluated at + runtime diff --git a/dev/include b/dev/include index d82fb74f22..0f43f00729 100644 --- a/dev/include +++ b/dev/include @@ -47,7 +47,6 @@ #install_printer (* univ full subst *) ppuniverse_level_subst;; #install_printer (* univ opt subst *) ppuniverse_opt_subst;; #install_printer (* evar univ ctx *) ppevar_universe_context;; -#install_printer (* constraints_map *) ppconstraints_map;; #install_printer (* inductive *) ppind;; #install_printer (* 'a scheme_kind *) ppscheme;; #install_printer (* type_judgement *) pptype;; @@ -62,7 +61,7 @@ (*#install_printer (* hints_path *) pphintspath;;*) #install_printer (* goal *) ppgoal;; (*#install_printer (* sigma goal *) ppsigmagoal;;*) -(*#install_printer (* proof *) pproof;;*) +#install_printer (* proof *) pproof;; #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* proofview *) ppproofview;; #install_printer (* metaset.t *) ppmetas;; diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f9310e076a..3850c05fd9 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -12,13 +12,15 @@ [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` +export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH + exec $OCAMLDEBUG \ - -I $CAMLP4LIB \ + -I $CAMLP4LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ + -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 \ @@ -30,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/printers.mllib b/dev/printers.mllib deleted file mode 100644 index 3165495488..0000000000 --- a/dev/printers.mllib +++ /dev/null @@ -1,219 +0,0 @@ -Coq_config - -Terminal -Hook -Canary -Hashset -Hashcons -CSet -CMap -Int -Dyn -HMap -Option -Store -Exninfo -Backtrace -IStream -Pp_control -Loc -CList -CString -Tok -Compat -Flags -Control -Loc -Serialize -Stateid -CObj -CArray -CStack -Util -Pp -Ppstyle -Richpp -Feedback -Segmenttree -Unicodetable -Unicode -CErrors -CWarnings -Bigint -CUnix -Minisys -System -Envars -Aux_file -Profile -Explore -Predicate -Rtree -Heap -Genarg -Stateid -CEphemeron -Future -RemoteCounter -Monad - -Names -Univ -UGraph -Esubst -Uint31 -Sorts -Evar -Constr -Context -Vars -Term -Mod_subst -Cbytecodes -Copcodes -Cemitcodes -Nativevalues -Primitives -Nativeinstr -Future -Opaqueproof -Declareops -Retroknowledge -Conv_oracle -Pre_env -Nativelambda -Nativecode -Nativelib -Cbytegen -Environ -CClosure -Reduction -Nativeconv -Type_errors -Modops -Inductive -Typeops -Fast_typeops -Indtypes -Cooking -Term_typing -Subtyping -Mod_typing -Nativelibrary -Safe_typing -Unionfind - -Summary -Nameops -Libnames -Globnames -Global -Nametab -Libobject -Lib -Loadpath -Goptions -Decls -Heads -Keys -Locusops -Miscops -Universes -Termops -Namegen -UState -Evd -Sigma -Glob_ops -Redops -Pretype_errors -Evarutil -Reductionops -Inductiveops -Arguments_renaming -Nativenorm -Retyping -Cbv - -Evardefine -Evarsolve -Recordops -Evarconv -Typing -Patternops -Constr_matching -Find_subterm -Tacred -Classops -Typeclasses_errors -Logic_monad -Proofview_monad -Proofview -Ftactic -Geninterp -Typeclasses -Detyping -Indrec -Program -Coercion -Cases -Pretyping -Unification -Declaremods -Library -States - -Genprint -CLexer -Ppextend -Pputils -Ppannotation -Stdarg -Constrarg -Constrexpr_ops -Genintern -Notation_ops -Notation -Dumpglob -Syntax_def -Smartlocate -Topconstr -Reserve -Impargs -Implicit_quantifiers -Constrintern -Modintern -Constrextern -Goal -Miscprint -Logic -Refiner -Clenv -Evar_refiner -Refine -Proof -Proof_global -Pfedit -Decl_mode -Ppconstr -Pcoq -Printer -Pptactic -Ppdecl_proof -Egramml -Egramcoq -Tacsubst -Trie -Dn -Btermdn -Hints -Himsg -ExplainErr -Locality -Assumptions -Vernacinterp -Dischargedhypsmap -Discharge -Declare -Ind_tables -Top_printers diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a3d5cf5c12..cd464801b0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pp x = Pp.pp_with !Pp_control.std_ft x +let pp x = Pp.pp_with !Topfmt.std_ft x (** Future printer *) @@ -200,7 +200,8 @@ let pppftreestate p = pp(print_pftreestate p) (* let ppsigmagoal g = pp(pr_goal (sig_it g)) *) (* let prgls gls = pp(pr_gls gls) *) (* let prglls glls = pp(pr_glls glls) *) -(* let pproof p = pp(print_proof Evd.empty empty_named_context p) *) + +let pproof p = pp(Proof.pr_proof p) let ppuni u = pp(pr_uni u) let ppuni_level u = pp (Level.pr u) @@ -233,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) @@ -502,7 +503,7 @@ END open Pcoq open Genarg -open Constrarg +open Stdarg open Egramml let _ = |