diff options
Diffstat (limited to 'dev')
47 files changed, 2171 insertions, 447 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..defea713d8 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,11 +17,13 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; +#directory "../API";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) +#load "API.cma";; #use "top_printers.ml";; #use "vm_printers.ml";; @@ -56,6 +58,8 @@ (* Open main files *) +open API +open Grammar_API open Names open Term open Vars @@ -147,9 +151,6 @@ open Refiner open Tacmach open Tactic_debug -open Decl_proof_instr -open Decl_mode - open Hints open Auto open Autorewrite @@ -195,7 +196,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/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 52b158871b..98e80c7652 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1082,7 +1082,7 @@ function make_coq { copq_coq_gtk copy_coq_license - # make clean seems to br broken for 8.5pl2 + # make clean seems to be broken for 8.5pl2 # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 0000000000..7f66dfb3b0 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,141 @@ +#!/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:=coq_makefile2-fix} +: ${UniMath_CI_GITURL:=https://github.com/maximedenes/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:=external-bignums} +: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git} + +: ${Corn_CI_BRANCH:=external-bignums} +: ${Corn_CI_GITURL:=https://github.com/letouzey/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 +######################################################################## +# Temporary overlay +: ${HoTT_CI_BRANCH:=ocaml.4.02.3} +: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} +# : ${HoTT_CI_BRANCH:=master} +# : ${HoTT_CI_GITURL:=https://github.com/HoTT/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:=less_init_plugins} +: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git} + +######################################################################## +# VST +######################################################################## +: ${VST_CI_BRANCH:=less_init_plugins} +: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git} + +######################################################################## +# fiat_parsers +######################################################################## +: ${fiat_parsers_CI_BRANCH:=trunk__API} +: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git} + +######################################################################## +# fiat_crypto +######################################################################## +: ${fiat_crypto_CI_BRANCH:=less_init_plugins} +: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git} + +######################################################################## +# bedrock_src +######################################################################## +: ${bedrock_src_CI_BRANCH:=master} +: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# bedrock_facade +######################################################################## +: ${bedrock_facade_CI_BRANCH:=master} +: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# formal-topology +######################################################################## +: ${formal_topology_CI_BRANCH:=ci} +: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} + +######################################################################## +# coq-dpdgraph +######################################################################## +: ${coq_dpdgraph_CI_BRANCH:=coq-trunk} +: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.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} + +######################################################################## +# Bignums +######################################################################## +: ${bignums_CI_BRANCH:=master} +: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh new file mode 100755 index 0000000000..95cfa3073f --- /dev/null +++ b/dev/ci/ci-bedrock-facade.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade + +git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR} + +( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade ) diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh new file mode 100755 index 0000000000..532611d4b3 --- /dev/null +++ b/dev/ci/ci-bedrock-src.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src + +git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR} + +( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src ) diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh new file mode 100755 index 0000000000..ff5935d4c7 --- /dev/null +++ b/dev/ci/ci-bignums.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}"]; +then + source ${ci_dir}/ci-common.sh +fi + +bignums_CI_DIR=${CI_BUILD_DIR}/Bignums + +git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR} + +( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh new file mode 100755 index 0000000000..a0a4e0749d --- /dev/null +++ b/dev/ci/ci-color.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Color_CI_DIR=${CI_BUILD_DIR}/color + +# Setup Bignums + +source ${ci_dir}/ci-bignums.sh + +# Compiles CoLoR + +svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} + +sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v + +# Adapt to PR #220 (FunInd not loaded in Prelude anymore) +sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v +sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v +sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v +sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v +sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v +sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v +sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v +sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v +sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v +sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v +sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v +sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v + +( cd ${Color_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh new file mode 100644 index 0000000000..f1e1515d41 --- /dev/null +++ b/dev/ci/ci-common.sh @@ -0,0 +1,73 @@ +#!/usr/bin/env bash + +set -xe + +if [ -n "${GITLAB_CI}" ]; +then + export COQBIN=`pwd`/install/bin +else + export COQBIN=`pwd`/bin +fi +export PATH="$COQBIN:$PATH" + +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN="$COQBIN/" + +ls "$COQBIN" + +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci + +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} + + # Allow an optional 4th argument for the commit + local _COMMIT=${4:-FETCH_HEAD} + local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi) + + mkdir -p ${_DEST} + ( cd ${_DEST} && \ + if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch ${_URL} ${_BRANCH} && \ + git checkout ${_COMMIT} && \ + 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 ${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 && \ + 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 new file mode 100755 index 0000000000..c78ffdc2c0 --- /dev/null +++ b/dev/ci/ci-compcert.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert + +opam install -j ${NJOBS} -y menhir +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} + +# Patch to avoid the upper version limit +( 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-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh new file mode 100755 index 0000000000..e8018158bf --- /dev/null +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph + +git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} + +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh new file mode 100755 index 0000000000..40eff03b78 --- /dev/null +++ b/dev/ci/ci-coquelicot.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot + +install_ssreflect + +git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} + +( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh new file mode 100755 index 0000000000..0e791ebbfd --- /dev/null +++ b/dev/ci/ci-cpdt.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +wget http://adam.chlipala.net/cpdt/cpdt.tgz +tar xvfz cpdt.tgz + +( cd cpdt && make clean && make -j ${NJOBS} ) + diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh new file mode 100755 index 0000000000..c6df45a1d4 --- /dev/null +++ b/dev/ci/ci-fiat-crypto.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto + +git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} + +( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} lite ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 0000000000..2095245eb8 --- /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 parsers-examples && make -j ${NJOBS} fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh new file mode 100755 index 0000000000..ec19bd9939 --- /dev/null +++ b/dev/ci/ci-flocq.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Flocq_CI_DIR=${CI_BUILD_DIR}/flocq + +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-formal-topology.sh b/dev/ci/ci-formal-topology.sh new file mode 100755 index 0000000000..64b78c0396 --- /dev/null +++ b/dev/ci/ci-formal-topology.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology + +# Setup Bignums + +source ${ci_dir}/ci-bignums.sh + +# 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} && make install ) + +# Setup formal-topology + +git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} + +( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh new file mode 100755 index 0000000000..4e5aa2687b --- /dev/null +++ b/dev/ci/ci-geocoq.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq + +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} + +( 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 && \ + sed -i.bak '/Elements\/Book_3\.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 new file mode 100755 index 0000000000..1bf6e9a872 --- /dev/null +++ b/dev/ci/ci-hott.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT + +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 new file mode 100755 index 0000000000..262dd6fa01 --- /dev/null +++ b/dev/ci/ci-iris-coq.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +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 Iris first, as it is needed to compute the dependencies + +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins + +# Setup stdpp +stdpp_CI_GITURL=${IRIS_DEP[1]}.git +stdpp_CI_COMMIT=${IRIS_DEP[2]} + +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} + +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) + +# Build iris now +( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh new file mode 100755 index 0000000000..46581c6381 --- /dev/null +++ b/dev/ci/ci-math-classes.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +# Setup Bignums + +source ${ci_dir}/ci-bignums.sh + +# 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 new file mode 100755 index 0000000000..bb8188da4e --- /dev/null +++ b/dev/ci/ci-math-comp.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +checkout_mathcomp ${mathcomp_CI_DIR} + +# odd_order takes too much time for travis. +( 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 new file mode 100755 index 0000000000..e31691179e --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq +metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq + +# Setup UniCoq + +git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} + +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) + +# 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 new file mode 100755 index 0000000000..23ef41d2dd --- /dev/null +++ b/dev/ci/ci-sf.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +# XXX: Needs fixing to properly set the build directory. +wget ${sf_CI_TARURL} +tar xvfz sf.tgz + +sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v + +( 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 new file mode 100755 index 0000000000..ce26399378 --- /dev/null +++ b/dev/ci/ci-tlc.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +tlc_CI_DIR=${CI_BUILD_DIR}/tlc + +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 new file mode 100755 index 0000000000..175b82b5f9 --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} + +( 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..2ecd40416f --- /dev/null +++ b/dev/ci/ci-user-overlay.sh @@ -0,0 +1,58 @@ +#!/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. + +echo $TRAVIS_PULL_REQUEST_BRANCH +echo $TRAVIS_PULL_REQUEST +echo $TRAVIS_BRANCH +echo $TRAVIS_COMMIT + +if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then + mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git +fi + +echo "DEBUG: ci-user-overlay.sh 0" +if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then + echo "DEBUG: ci-user-overlay.sh 1" + bedrock_src_CI_BRANCH=trunk__API + bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git + bedrock_facade_CI_BRANCH=trunk__API + bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git + fiat_parsers_CI_BRANCH=trunk__API + fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git +fi + +if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then + math_classes_CI_BRANCH=external-bignums + math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git + Corn_CI_BRANCH=external-bignums + Corn_CI_GITURL=https://github.com/letouzey/corn.git +fi + +if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then + CompCert_CI_BRANCH=less_init_plugins + CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git + VST_CI_BRANCH=less_init_plugins + VST_CI_GITURL=https://github.com/letouzey/VST.git + fiat_crypto_CI_BRANCH=less_init_plugins + fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git +fi diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 0000000000..c111951852 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +VST_CI_DIR=${CI_BUILD_DIR}/VST + +# opam install -j ${NJOBS} -y menhir +git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} + +# Targets are: msl veric floyd +# Patch to avoid the upper version limit +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) diff --git a/dev/core.dbg b/dev/core.dbg new file mode 100644 index 0000000000..71d06cdb0a --- /dev/null +++ b/dev/core.dbg @@ -0,0 +1,22 @@ +source camlp4.dbg +load_printer threads.cma +load_printer str.cma +load_printer clib.cma +load_printer lib.cma +load_printer dynlink.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 intf.cma +load_printer API.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 @@ -27,6 +28,7 @@ install_printer Top_printers.pppattern install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr +install_printer Top_printers.ppeconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses install_printer Top_printers.ppconstraints 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..0728608f31 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,294 @@ ========================================= += 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 * + +Added two functions for declaring hooks to be executed in reduction +functions when some given constants are traversed: + + declare_reduction_effect: to declare a hook to be applied when some + constant are visited during the execution of some reduction functions + (primarily cbv). + + set_reduction_effect: to declare a constant on which a given effect + hook should be called. + +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. + +The following types have been moved and modified: + + local_binder -> local_binder_expr + glob_binder merged with glob_decl + +The following constructors have been renamed: + + LocalRawDef -> CLocalDef + LocalRawAssum -> CLocalAssum + LocalPattern -> CLocalPattern + +In Constrexpr_ops: + + Deprecating abstract_constr_expr in favor of mkCLambdaN, and + prod_constr_expr in favor of mkCProdN. Note: the first ones were + interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second + ones were preserving the original sharing of the type. + +In Nameops: + + The API has been made more uniform. New combinators added in the + "Name" space name. Function "out_name" now fails with IsAnonymous + rather than with Failure "Nameops.out_name". + +Location handling and AST attributes: + + Location handling has been reworked. First, Loc.ghost has been + removed in favor of an option type, all objects carrying an optional + source code location have been switched to use `Loc.t option`. + + Storage of location information has been also refactored. The main + datatypes representing Coq AST (constrexpr, glob_expr) have been + switched to a generic "node with attributes" representation `'a + CAst.ast`, which is a record of the form: + +```ocaml +type 'a ast = private { + v : 'a; + loc : Loc.t option; + ... +} +``` + consumers of AST nodes are recommended to use accessor-based pattern + matching `{ v; loc }` to destruct `ast` object. Creation is done + with `CAst.make ?loc obj`, where the attributes are optional. Some + convenient combinators are provided in the module. A typical match: +``` +| CCase(loc, a1) -> CCase(loc, f a1) +``` + is now done as: +``` +| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) +``` + or even better, if plan to preserve the attributes you can wrap your + top-level function in `CAst.map` to have: + +``` +| CCase(a1) -> CCase(f a1) +``` + + This scheme based on records enables easy extensibility of the AST + node type without breaking compatibility. + + Not all objects carrying a location have been converted to the + generic node representation, some of them may be converted in the + future, for some others the abstraction is not just worth it. + + Thus, we still maintain a `'a Loc.located == Loc.t option * a'`, + tuple type which should be treated as private datatype (ok to match + against, but forbidden to manually build), and it is mandatory to + use it for objects that carry a location. This policy has been + implemented in the whole code base. Matching a located object hasn't + changed, however, `Loc.tag ?loc obj` must be used to build one. + +In GOption: + + Support for non-synchronous options has been removed. Now all + options are handled as a piece of normal document state, and thus + passed to workers, etc... As a consequence, the field + `Goptions.optsync` has been removed. + +In Coqlib / reference location: + + We have removed from Coqlib functions returning `constr` from + names. Now it is only possible to obtain references, that must be + processed wrt the particular needs of the client. + We have changed in constrintern the functions returnin `constr` as + well to return global references instead. + + Users of `coq_constant/gen_constant` can do + `Universes.constr_of_global (find_reference dir r)` _however_ note + the warnings in the `Universes.constr_of_global` in the + documentation. It is very likely that you were previously suffering + from problems with polymorphic universes due to using + `Coqlib.coq_constant` that used to do this. You must rather use + `pf_constr_of_global` in tactics and `Evarutil.new_global` variants + when constructing terms in ML (see univpoly.txt for more information). + +** Tactic API ** + +- pf_constr_of_global now returns a tactic instead of taking a continuation. + Thus it only generates one instance of the global reference, and it is the + caller's responsibility to perform a focus on the goal. + +- pf_global, construct_reference, global_reference, + global_reference_in_absolute_module now return a global_reference + instead of a constr. + +- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase + was very specific. Use tclPROGRESS instead. + +- The unsafe flag of the Refine.refine function and its variants has been + renamed and dualized into typecheck and has been made mandatory. + +** 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. + +** Additional changes in tactic extensions ** + +Entry "constr_with_bindings" has been renamed into +"open_constr_with_bindings". New entry "constr_with_bindings" now +uses type classes and rejects terms with unresolved holes. + +** 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` and `error` 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 + +** Stm API ** + +- We have streamlined the `Stm` API, now `add` and `query` take a + `coq_parsable` instead a `string` so clients can have more control + over their input stream. As a consequence, their types have been + modified. + +- The main parsing entry point has also been moved to the + `Stm`. Parsing is considered a synchronous operation so it will + either succeed or raise an exception. + +- `Feedback` is now only emitted for asynchronous operations. As a + consequence, it always carries a valid stateid and the type has + changed to accommodate that. + +- A few unused hooks were removed due to cleanups, no clients known. + +** Toplevel and Vernacular API ** + +- The components related to vernacular interpretation have been moved + to their own folder `vernac/` whereas toplevel now contains the + proper toplevel shell and compiler. + +- Coq's toplevel has been ported to directly use the common `Stm` + API. The signature of a few functions has changed as a result. + +** XML Protocol ** + +- The legacy `Interp` call has been turned into a noop. + +========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd index f2314e224f..cc33efd483 100644 --- a/dev/doc/cic.dtd +++ b/dev/doc/cic.dtd @@ -125,7 +125,7 @@ id ID #REQUIRED sort %sort; #REQUIRED> -<!-- The substitutions are ordered by increasing DeBrujin --> +<!-- The substitutions are ordered by increasing de Bruijn --> <!-- index. An empty substitution means that that index is --> <!-- not accessible. --> <!ELEMENT META (substitution*)> 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/econstr.md b/dev/doc/econstr.md new file mode 100644 index 0000000000..bb17e8fb62 --- /dev/null +++ b/dev/doc/econstr.md @@ -0,0 +1,129 @@ +# Evar-insensitive terms (EConstr) + +Evar-insensitive terms were introduced in 8.7, following +[CEP #10](https://github.com/coq/ceps/blob/master/text/010-econstr.md). We will +not recap the motivations in this document and rather summarize the code changes +to perform. + +## Overview + +The essential datastructures are defined in +[the `EConstr` module](/engine/eConstr.mli) module. It defines +the tactic counterparts of kernel data structures such as terms +(`EConstr.constr`), universes (`EConstr.ESorts.t`) and contexts +(`EConstr.*_context`). + +The main difference with kernel-side types is that observing them requires +an evar-map at hand in order to normalize evars on the fly. The basic primitive +to observe an `EConstr.t` is the following function: +``` +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term +(** Same as {!Constr.kind} except that it expands evars and normalizes + universes on the fly. *) +``` + +Essentially, each time it sees an evar which happens to be defined in the +provided evar-map, it replaces it with the corresponding body and carries on. + +Due to universe unification occuring at the tactic level, the same goes for +universe instances and sorts. See the `ESort` and `EInstance` modules in +`EConstr`. + +This normalization is critical for the soundness of tactics. Before EConstr, a +lot of bugs were lurking in the code base, a few still are (most notably in +meta-based unification) and failure to respect the guidelines thereafter may +result in nasal demons. + +## Transition path + +### Types + +As a rule of thumb, all functions living at the tactic level should manipulate +`EConstr.t` instead of `Constr.t`, and similarly for the other data structures. + +To ease the transition, the `EConstr` module defines a handful of aliases to +shadow the type names from the kernel. + +It is recommended to perform the following replacement in headers. +```ocaml +(** Kernel types. You may remove the two following opens if you want. Beware + that [kind_of_term] needs to be in scope if you use [EConstr.kind] so that + you may still need to open one of the two. *) +open Term +open Constr +(** Tactic types. Open this after to shadow kernel types. *) +open EConstr +``` + +Note that the `EConstr` module also redefines a `Vars` submodule. + +### Evar-map-passing + +All functions deconstructing an econstr need to take an evar-map as a parameter. +Therefore, you need to pass one as an argument virtually everywhere. + +In the Coq source code, it is recommended to take the evar-map as a first +argument called `sigma`, except if the function also takes an environment in +which case it is passed second. Namely, the two typical instances are: +```ocaml +let foo sigma c = mycode +val foo : Evd.evar_map -> EConstr.t -> Foo.t + +let bar env sigma c = mycode +val bar : Environ.env -> Evd.evar_map -> EConstr.t -> Bar.t +``` + +The EConstr API makes the code much more sensitive to evar-maps, because a +lot of now useless normalizations were removed. Thus one should be cautious of +**not** dropping the evar-map when it has been updated, and should rather stick +to a strict state-passing discipline. Unsound primitives like +`Typing.unsafe_type_of` are also a known source of problems, so you should +replace them with the corresponding evar-map-returning function and thread it +properly. + +### Functions + +Many functions from `Constr` and `Term` are redefined to work on econstr in +the `EConstr` module, so that it is often enough to perform the `open` as +described above to replace them. Their type may differ though, because they now +need access to an evar-map. A lot of econstr-manipulating functions are also +defined in [`Termops`](/engine/termops.mli). + +Functions manipulating tactic terms and kernel terms share the same name if they +are the equivalent one of the other. Do not hesitate to grep Coq mli files to +find the equivalent of a function you want to port if it is neither in `EConstr` +nor in `Termops` (this should be very rare). + +### Conversion + +Sometimes you do not have any other choice than calling kernel-side functions +on terms, and conversely to turn a kernel term into a tactic term. + +There are two functions to do so. +* `EConstr.of_constr` turns kernel terms into tactic terms. It is currently +the physical identity, and thus O(1), but this may change in the future. +* `EConstr.to_constr` turns tactic terms into kernel terms. It performs a +full-blown normalization of the given term, which is O(n) and potentially +costly. + +For performance reasons, avoiding to jump back and forth between kernel and +tactic terms is recommended. + +There are also a few unsafe conversion functions that take advantage of the +fact that `EConstr.t` is internally the same as `Constr.t`. Namely, +`EConstr.Unsafe.to_constr` is the physical identity. It should **not** be used +in typical code and is instead provided for efficiency **when you know what you +are doing**. Either use it to reimplement low-level functions that happen to +be insensitive externally, or use it to provide backward compatibility with +broken code that relies on evar-sensitivity. **Do not use it because it is +easier than stuffing evar-maps everywhere.** You've been warned. + +## Notes + +The EConstr branch fixed a lot of eisenbugs linked to lack of normalization +everywhere, most notably in unification. It may also have introduced a few, so +if you see a change in behaviour *that looks like a bug*, please report it. +Obviously, unification is not specified, so it's hard to tell apart, but still. + +Efficiency has been affected as well. We now pay an overhead when observing a +term, but at the same time a lot of costly upfront normalizations were removed. diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md new file mode 100644 index 0000000000..8f96ac223f --- /dev/null +++ b/dev/doc/proof-engine.md @@ -0,0 +1,133 @@ +Tutorial on the new proof engine for ML tactic writers +====================================================== + +Starting from Coq 8.5, a new proof engine has been introduced, replacing the old +meta-based engine which had a lot of drawbacks, ranging from expressivity to +soundness, the major one being that the type of tactics was transparent. This +was pervasively abused and made virtually impossible to tweak the implementation +of the engine. + +The old engine is deprecated and is slowly getting removed from the source code. + +The new engine relies on a monadic API defined in the `Proofview` module. Helper +functions and higher-level operations are defined in the `Tacmach` and +`Tacticals` modules, and end-user tactics are defined amongst other in the +`Tactics` module. + +At the root of the engine is a representation of proofs as partial terms that +can contain typed holes, called evars, short for *existential variable*. An evar +is essentially defined by its context and return type, that we will write +`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type +`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by +applying `EConstr.mkEvar`, and which we will write `?e{σ}`. + +The engine monad features a notion of global state called `evar_map`, defined in +the `Evd` module, which is the structure containing the incremental refinement +of evars. `Evd` is a low-level API and its use is discouraged in favour of the +`Evarutil` module which provides more abstract primitives. + +In addition to this state, the monad also features a goal state, that is +an ordered list of current holes to be filled. While these holes are referred +to as goals at a high-enough level, they are actually no more than evars. The +API provided to deal with these holes can be found in the `Proofview.Goal` +module. Tactics are naturally operating on several goals at once, so that it is +usual to use the `Proofview.Goal.enter` function and its variants to dispatch a +tactic to each of the goals under focus. + +Primitive tactics by term refining +------------------------------------- + +A typical low-level tactic will be defined by plugging partial terms in the +goal holes thanks to the `Refine` module, and in particular to the +`Refine.refine` primitive. + +```ocaml +val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine typecheck t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) +``` + +In a first approximation, we can think of `'a Sigma.run` as +`evar_map -> 'a * evar_map`. What the function does is first evaluate the +`Constr.t Sigma.run` argument in the current proof state, and then use the +resulting term as a filler for the proof under focus. All evars that have been +created by the invocation of this thunk are then turned into new goals added in +the order of their creation. + +To see how we can use it, let us have a look at an idealized example, the `cut` +tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` +with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and +`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and +two new holes `[e1, e2]` are added to the goal state in this order. + +```ocaml +let cut c = + let open Sigma in + Proofview.Goal.nf_enter { enter = begin fun gl -> + (** In this block, we focus on one goal at a time indicated by gl *) + let env = Proofview.Goal.env gl in + (** Get the context of the goal, essentially [Γ] *) + let concl = Proofview.Goal.concl gl in + (** Get the conclusion [A] of the goal *) + let hyps = Tacmach.New.pf_ids_of_hyps gl in + (** List of hypotheses from the context of the goal *) + let id = Namegen.next_name_away Anonymous hyps in + (** Generate a fresh identifier *) + let t = mkArrow c (Vars.lift 1 concl) in + (** Build [X -> A]. Note the lifting of [A] due to being on the right hand + side of the arrow. *) + Refine.refine { run = begin fun sigma -> + (** All evars generated by this block will be added as goals *) + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the + term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity + substitution for [Γ] is extracted from the [env] argument, so that + one must be careful to pass the correct context here in order for the + resulting term to be well-typed. The [p] return value is a proof term + used to enforce sigma monotonicity. *) + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return + [x := Γ ⊢ ?e2{Γ} : X]. *) + let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in + (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) + Sigma (r, sigma, p +> q) + (** Fills the current hole with [r]. The [p +> q] thingy ensures + monotonicity of sigma. *) + end } + end } +``` + +The `Evarutil.new_evar` function is the preferred way to generate evars in +tactics. It returns a ready-to-use term, so that one does not have to call +the `mkEvar` primitive. There are lower-level variants whose use is dedicated to +special use cases, *e.g.* whenever one wants a non-identity substitution. One +should take care to call it with the proper `env` argument so that the evar +and term it generates make sense in the context they will be plugged in. + +For the sake of completeness, the old engine was relying on the `Tacmach.refine` +function to provide a similar feature. Nonetheless, it was using untyped metas +instead of evars, so that it had to mangle the argument term to actually produce +the term that would be put into the hole. For instance, to work around the +untypedness, some metas had to be coerced with a cast to enforce their type, +otherwise leading to runtime errors. This was working for very simple +instances, but was unreliable for everything else. + +High-level composition of tactics +------------------------------------ + +It is possible to combine low-level refinement tactics to create more powerful +abstractions. While it was the standard way of doing things in the old engine +to overcome its technical limitations (namely that one was forced to go through +a limited set of derivation rules), it is recommended to generate proofs as +much as possible by refining in ML tactics when it is possible and easy enough. +Indeed, this prevents dependence on fragile constructions such as unification. + +Obviously, it does not forbid the use of tacticals to mimick what one would do +in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple +semantics. A list of such tacticals can be found in the `Tacticals` module. Most +of them are a porting of the tacticals from the old engine to the new one, so +that if they share the same name they are expected to have the same semantics. 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/doc/xml-protocol.md b/dev/doc/xml-protocol.md new file mode 100644 index 0000000000..2ff82c6888 --- /dev/null +++ b/dev/doc/xml-protocol.md @@ -0,0 +1,745 @@ +#Coq XML Protocol for Coq 8.6# + +This document is based on documentation originally written by CJ Bell +for his [vscoq](https://github.com/siegebell/vscoq/) project. + +Here, the aim is to provide a "hands on" description of the XML +protocol that coqtop and IDEs use to communicate. The protocol first appeared +with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming +versions of Proof General. + +A somewhat out-of-date description of the async state machine is +[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). +OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). + +# CHANGES +## Changes from 8.5: + * In several places, flat text wrapped in <string> tags now appears as structured text inside <richpp> tags + * The "errormsg" feedback has been replaced by a "message" feedback which contains + <feedback\_content> tag, with a message_level attribute of "error" + +* [Commands](#commands) + - [About](#command-about) + - [Add](#command-add) + - [EditAt](#command-editAt) + - [Init](#command-init) + - [Goal](#command-goal) + - [Status](#command-status) + - [Query](#command-query) + - [Evars](#command-evars) + - [Hints](#command-hints) + - [Search](#command-search) + - [GetOptions](#command-getoptions) + - [SetOptions](#command-setoptions) + - [MkCases](#command-mkcases) + - [StopWorker](#command-stopworker) + - [PrintAst](#command-printast) + - [Annotate](#command-annotate) +* [Feedback messages](#feedback) + - [Added Axiom](#feedback-addedaxiom) + - [Processing](#feedback-processing) + - [Processed](#feedback-processed) + - [Incomplete](#feedback-incomplete) + - [Complete](#feedback-complete) + - [GlobRef](#feedback-globref) + - [Error](#feedback-error) + - [InProgress](#feedback-inprogress) + - [WorkerStatus](#feedback-workerstatus) + - [File Dependencies](#feedback-filedependencies) + - [File Loaded](#feedback-fileloaded) + - [Message](#feedback-message) + - [Custom](#feedback-custom) + +Sentences: each command sent to Coqtop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF). +Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity." +In practice, the command sentences sent to Coqtop are terminated at the "." and start with any previous whitespace. +Each sentence is assigned a unique stateId after being sent to Coq (via Add). +States: + * Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing) + * Processed: + * InProgress: + * Incomplete: the validity of the sentence cannot be checked due to a prior error + * Complete: + * Error: the sentence has an error + +State ID 0 is reserved as a 'dummy' state. + +-------------------------- + +## <a name="commands">Commands</a> + +### <a name="command-about">**About(unit)**</a> +Returns information about the protocol and build dates for Coqtop. +``` +<call val="About"> + <unit/> +</call> +``` +#### *Returns* +```html + <value val="good"> + <coq_info><string>8.6</string> + <string>20150913</string> + <string>December 2016</string> + <string>Dec 23 2016 16:16:30</string> + </coq_info> +</value> +``` +The string fields are the Coq version, the protocol version, the release date, and the compile time of Coqtop. +The protocol version is a date in YYYYMMDD format, where "20150913" corresponds to Coq 8.6. An IDE that wishes +to support multiple Coq versions can use the protocol version information to know how to handle output from Coqtop. + +### <a name="command-add">**Add(stateId: integer, command: string, verbose: boolean)**</a> +Adds a toplevel command (e.g. vernacular, definition, tactic) to the given state. +`verbose` controls whether out-of-band messages will be generated for the added command (e.g. "foo is assumed" in response to adding "Axiom foo: nat."). +```html +<call val="Add"> + <pair> + <pair> + <string>${command}</string> + <int>${editId}</int> + </pair> + <pair> + <state_id val="${stateId}"/> + <bool val="${verbose}"/> + </pair> + </pair> +</call> +``` + +#### *Returns* +* The added command is given a fresh `stateId` and becomes the next "tip". +```html +<value val="good"> + <pair> + <state_id val="${newStateId}"/> + <pair> + <union val="in_l"><unit/></union> + <string>${message}</string> + </pair> + </pair> +</value> +``` +* When closing a focused proof (in the middle of a bunch of interpreted commands), +the `Qed` will be assigned a prior `stateId` and `nextStateId` will be the id of an already-interpreted +state that should become the next tip. +```html +<value val="good"> + <pair> + <state_id val="${stateId}"/> + <pair> + <union val="in_r"><state_id val="${nextStateId}"/></union> + <string>${message}</string> + </pair> + </pair> +</value> +``` +* Failure: + - Syntax error. Error offsets are byte offsets (not character offsets) with respect to the start of the sentence, starting at 0. + ```html + <value val="fail" + loc_s="${startOffsetOfError}" + loc_e="${endOffsetOfError}"> + <state_id val="${stateId}"/> + <richpp>${errorMessage}</richpp> + </value> + ``` + - Another kind of error, for example, Qed with a pending goal. + ```html + <value val="fail"><state_id val="${stateId}"/><richpp>${errorMessage}</richpp></value> + ``` + +------------------------------- + +### <a name="command-editAt">**EditAt(stateId: integer)**</a> +Moves current tip to `${stateId}`, such that commands may be added to the new state ID. +```html +<call val="Edit_at"><state_id val="${stateId}"/></call> +``` +#### *Returns* +* Simple backtrack; focused stateId becomes the parent state +```html +<value val="good"> + <union val="in_l"><unit/></union> +</value> +``` + +* New focus; focusedQedStateId is the closing Qed of the new focus; senteneces between the two should be cleared +```html +<value val="good"> + <union val="in_r"> + <pair> + <state_id val="${focusedStateId}"/> + <pair> + <state_id val="${focusedQedStateId}"/> + <state_id val="${oldFocusedStateId}"/> + </pair> + </pair> + </union> +</value> +``` +* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of ``stateId` that shopuld be edited instead. +```html +<value val="fail" loc_s="${startOffsetOfError}" loc_e="${endOffsetOfError}"> + <state_id val="${errorFreeStateId}"/> + ${errorMessage} +</value> +``` + +------------------------------- + +### <a name="command-init">**Init()**</a> +* No options. +```html +<call val="Init"><option val="none"/></call> +``` +* With options. Looking at + [ide_slave.ml](https://github.com/coq/coq/blob/c5d0aa889fa80404f6c291000938e443d6200e5b/ide/ide_slave.ml#L355), + it seems that `options` is just the name of a script file, whose path + is added via `Add LoadPath` to the initial state. +```html +<call val="Init"> + <option val="some"> + <string>${options}</string> + </option> +</call> +``` +Providing the script file enables Coq to use .aux files created during +compilation. Those file contain timing information that allow Coq to +choose smartly between asynchronous and synchronous processing of +proofs. + +#### *Returns* +* The initial stateId (not associated with a sentence) +```html +<value val="good"> + <state_id val="${initialStateId}"/> +</value> +``` + +------------------------------- + + +### <a name="command-goal">**Goal()**</a> +```html +<call val="Goal"><unit/></call> +``` +#### *Returns* +* If there is a goal. `shelvedGoals` and `abandonedGoals` have the same structure as the first set of (current/foreground) goals. `backgroundGoals` contains a list of pairs of lists of goals (list ((list Goal)*(list Goal))); it represents a "focus stack" ([see code for reference](https://github.com/coq/coq/blob/trunk/engine/proofview.ml#L113)). Each time a proof is focused, it will add a new pair of lists-of-goals. The first pair is the most nested set of background goals, the last pair is the top level set of background goals. The first list in the pair is in reverse order. Each time you focus the goal (e.g. using `Focus` or a bullet), a new pair will be prefixed to the list. +```html +<value val="good"> + <option val="some"> + <goals> + <!-- current goals --> + <list> + <goal> + <string>3</string> + <list> + <richpp>${hyp1}</richpp> + ... + <richpp>${hypN}</richpp> + </list> + <richpp>${goal}</richpp> + </goal> + ... + ${goalN} + </list> + <!-- `backgroundGoals` --> + <list> + <pair> + <list><goal />...</list> + <list><goal />...</list> + </pair> + ... + </list> + ${shelvedGoals} + ${abandonedGoals} + </goals> + </option> +</value> +``` + +For example, this script: +```coq +Goal P -> (1=1/\2=2) /\ (3=3 /\ (4=4 /\ 5=5) /\ 6=6) /\ 7=7. +intros. +split; split. (* current visible goals are [1=1, 2=2, 3=3/\(4=4/\5=5)/\6=6, 7=7] *) +Focus 3. (* focus on 3=3/\(4=4/\5=5)/\6=6; bg-before: [1=1, 2=2], bg-after: [7=7] *) +split; [ | split ]. (* current visible goals are [3=3, 4=4/\5=5, 6=6] *) +Focus 2. (* focus on 4=4/\5=5; bg-before: [3=3], bg-after: [6=6] *) +* (* focus again on 4=4/\5=5; bg-before: [], bg-after: [] *) +split. (* current visible goals are [4=4,5=5] *) +``` +should generate the following goals structure: +``` +goals: [ P|-4=4, P|-5=5 ] +background: +[ + ( [], [] ), (* bullet with one goal has no before or after background goals *) + ( [ P|-3=3 ], [ P|-6=6 ] ), (* Focus 2 *) + ( [ P|-2=2, P|-1=1 ], [ P|-7=7 ] ) (* Focus 3; notice that 1=1 and 2=2 are reversed *) +] +``` +Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ++ goals ++ flat_map snd background`. + +* No goal: +```html +<value val="good"><option val="none"/></value> +``` + +------------------------------- + + +### <a name="command-status">**Status(force: bool)**</a> +CoqIDE typically sets `force` to `false`. +```html +<call val="Status"><bool val="${force}"/></call> +``` +#### *Returns* +* +```html +<status> + <string>${path}</string> + <string>${proofName}</string> + <string>${allProofs}</string> + <string>${proofNumber}</string> +</status> +``` + +------------------------------- + + +### <a name="command-query">**Query(query: string, stateId: integer)**</a> +In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state. +```html +<call val="Query"> + <pair> + <string>${query}</string> + <state_id val="${stateId}"/> + </pair> +</call> +``` +#### *Returns* +* +```html +<value val="good"> + <string>${message}</string> +</value> +``` +------------------------------- + + + +### <a name="command-evars">**Evars()**</a> +```html +<call val="Evars"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <option val="some"> + <list> + <evar>${evar1}</evar> + ... + <evar>${evarN}</evar> + </list> + </option> +</value> +``` + +------------------------------- + + +### <a name="command-hints">**Hints()**</a> +```html +<call val="Hints"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <option val="some"> + <pair> + <list/> + <list> + <pair> + <string>${hint1}</string> + <string>${hint2}</string> + </pair> + ... + <pair> + <string>${hintN-1}</string> + <string>${hintN}</string> + </pair> + </list> + </pair> + </option> +</value> +``` + +------------------------------- + + +### <a name="command-search">**Search([(constraintTypeN: string, constraintValueN: string, positiveConstraintN: boolean)])**</a> +Searches for objects that satisfy a list of constraints. If `${positiveConstraint}` is `false`, then the constraint is inverted. +```html +<call val="Search"> + <list> + <pair> + <search_cst val="${constraintType1}"> + ${constraintValue1} + </search_cst> + <bool val="${positiveConstraint1}"/> + </pair> + ... + <!-- Example: --> + <pair> + <search_cst val="name_pattern"> + <string>bool_rect</string> + </search_cst> + <bool val="true"/> + </pair> + </list> +</call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <coq_object> + <list> + <string>${metaInfo}</string> + ... + </list> + <list> + <string>${name}</string> + </list> + <string>${definition}</string> + </coq_object> + ... + </list> +</value> +``` +##### Types of constraints: +* Name pattern: `${constraintType} = "name_pattern"`; `${constraintValue}` is a regular expression string. +* Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure. +* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*. + +------------------------------- + + +### <a name="command-getoptions">**GetOptions()**</a> +```html +<call val="GetOptions"><unit/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <pair> + <list><string>${string1}</string>...</list> + <option_state> + <bool>${sync}</bool> + <bool>${deprecated}</bool> + <string>${name}</string> + ${option_value} + </option_state> + </pair> + ... + </list> +</value> +``` + +------------------------------- + + +### <a name="command-setoptions">**SetOptions(options)**</a> +Sends a list of option settings, where each setting roughly looks like: +`([optionNamePart1, ..., optionNamePartN], value)`. +```html +<call val="SetOptions"> + <list> + <pair> + <list> + <string>optionNamePart1</string> + ... + <string>optionNamePartN</string> + </list> + <option_value val="${typeOfOption}"> + <option val="some"> + ${value} + </option> + </option_value> + </pair> + ... + <!-- Example: --> + <pair> + <list> + <string>Printing</string> + <string>Width</string> + </list> + <option_value val="intvalue"> + <option val="some"><int>60</int></option> + </option_value> + </pair> + </list> +</call> +``` +CoqIDE sends the following settings (defaults in parentheses): +``` +Printing Width : (<option_value val="intvalue"><int>60</int></option_value>), +Printing Coercions : (<option_value val="boolvalue"><bool val="false"/></option_value>), +Printing Matching : (...true...) +Printing Notations : (...true...) +Printing Existential Instances : (...false...) +Printing Implicit : (...false...) +Printing All : (...false...) +Printing Universes : (...false...) +``` +#### *Returns* +* +```html +<value val="good"><unit/></value> +``` + +------------------------------- + + +### <a name="command-mkcases">**MkCases(...)**</a> +```html +<call val="MkCases"><string>...</string></call> +``` +#### *Returns* +* +```html +<value val="good"> + <list> + <list><string>${string1}</string>...</list> + ... + </list> +</value> +``` + +------------------------------- + + +### <a name="command-stopworker">**StopWorker(worker: string)**</a> +```html +<call val="StopWorker"><string>${worker}</string></call> +``` +#### *Returns* +* +```html +<value val="good"><unit/></value> +``` + +------------------------------- + + +### <a name="command-printast">**PrintAst(stateId: integer)**</a> +```html +<call val="PrintAst"><state_id val="${stateId}"/></call> +``` +#### *Returns* +* +```html +<value val="good"> + <gallina begin="${gallina_begin}" end="${gallina_end}"> + <theorem begin="${theorem_begin}" end="${theorem_end}" type="Theorem" name="${theorem_name}"> + <apply begin="${apply_begin}" end="${apply_end}"> + <operator begin="${operator_begin}" end="${operator_end}" name="${operator_name}"/> + <typed begin="${typed_begin}" end="${typed_end}"> + <constant begin="${constant_begin}" end="${constant_end}" name="${constant_name}"/> + ... + <token begin="${token_begin}" end="token_end">${token}</token> + ... + </typed> + ... + </apply> + </theorem> + ... + </gallina> +</value> +``` + +------------------------------- + + + +### <a name="command-annotate">**Annotate(annotation: string)**</a> +```html +<call val="Annotate"><string>${annotation}</string></call> +``` +#### *Returns* +* + +take `<call val="Annotate"><string>Theorem plus_0_r : forall n : nat, n + 0 = n.</string></call>` as an example. + +```html +<value val="good"> + <pp startpos="0" endpos="45"> + <vernac_expr startpos="0" endpos="44"> + <keyword startpos="0" endpos="7">Theorem</keyword> + plus_0_r : + <constr_expr startpos="19" endpos="44"> + <keyword startpos="19" endpos="25">forall</keyword> + n : + <constr_expr startpos="30" endpos="33">nat</constr_expr> + , + <unparsing startpos="35" endpos="44"> + <unparsing startpos="35" endpos="40"> + <unparsing startpos="35" endpos="40"> + <unparsing startpos="35" endpos="36"> + <constr_expr startpos="35" endpos="36">n</constr_expr> + </unparsing> + <unparsing startpos="36" endpos="38"> +</unparsing> + <unparsing startpos="38" endpos="39"> </unparsing> + <unparsing startpos="39" endpos="40"> + <constr_expr startpos="39" endpos="40">0</constr_expr> + </unparsing> + </unparsing> + </unparsing> + <unparsing startpos="40" endpos="42"> =</unparsing> + <unparsing startpos="42" endpos="43"> </unparsing> + <unparsing startpos="43" endpos="44"> + <constr_expr startpos="43" endpos="44">n</constr_expr> + </unparsing> + </unparsing> + </constr_expr> + </vernac_expr> + . + </pp> +</value> +``` + +------------------------------- + +## <a name="feedback">Feedback messages</a> + +Feedback messages are issued out-of-band, + giving updates on the current state of sentences/stateIds, + worker-thread status, etc. + +In the descriptions of feedback syntax below, wherever a `state_id` +tag may occur, there may instead be an `edit_id` tag. + +* <a name="feedback-addedaxiom">Added Axiom</a>: in response to `Axiom`, `admit`, `Admitted`, etc. +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="addedaxiom" /> +</feedback> +``` +* <a name="feedback-processing">Processing</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="processingin"> + <string>${workerName}</string> + </feedback_content> +</feedback> +``` +* <a name="feedback-processed">Processed</a> +```html +<feedback object="state" route="0"> + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="processed"/> +</feedback> +``` +* <a name="feedback-incomplete">Incomplete</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="incomplete" /> +</feedback> +``` +* <a name="feedback-complete">Complete</a> +* <a name="feedback-globref">GlobRef</a> +* <a name="feedback-error">Error</a>. Issued, for example, when a processed tactic has failed or is unknown. +The error offsets may both be 0 if there is no particular syntax involved. +* <a name="feedback-inprogress">InProgress</a> +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="inprogress"> + <int>1</int> + </feedback_content> +</feedback> +``` +* <a name="feedback-workerstatus">WorkerStatus</a> +Ex: `workername = "proofworker:0"` +Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"` +```html +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="workerstatus"> + <pair> + <string>${workerName}</string> + <string>${status}</string> + </pair> + </feedback_content> +</feedback> +``` +* <a name="feedback-filedependencies">File Dependencies</a>. Typically in response to a `Require`. Dependencies are *.vo files. + - State `stateId` directly depends on `dependency`: + ```html + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="filedependency"> + <option val="none"/> + <string>${dependency}</string> + </feedback_content> + </feedback> + ``` + - State `stateId` depends on `dependency` via dependency `sourceDependency` + ```xml + <feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="filedependency"> + <option val="some"><string>${sourceDependency}</string></option> + <string>${dependency}</string> + </feedback_content> + </feedback> + ``` +* <a name="feedback-fileloaded">File Loaded</a>. For state `stateId`, module `module` is being loaded from `voFileName` +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="fileloaded"> + <string>${module}</string> + <string>${voFileName`}</string> + </feedback_content> +</feedback> +``` + +* <a name="feedback-message">Message</a>. `level` is one of `{info,warning,notice,error,debug}`. For example, in response to an <a href="#command-add">add</a> `"Axiom foo: nat."` with `verbose=true`, message `foo is assumed` will be emitted in response. +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="message"> + <message> + <message_level val="${level}"/> + <string>${message}</string> + </message> + </feedback_content> +</feedback> +``` + +* <a name="feedback-custom">Custom</a>. A feedback message that Coq plugins can use to return structured results, including results from Ltac profiling. Optionally, `startPos` and `stopPos` define a range of offsets in the document that the message refers to; otherwise, they will be 0. `customTag` is intended as a unique string that identifies what kind of payload is contained in `customXML`. +```xml +<feedback object="state" route="0"> + <state_id val="${stateId}"/> + <feedback_content val="custom"> + <loc start="${startPos}" stop="${stopPos}"/> + <string>${customTag}</string> + ${customXML} + </feedback_content> +</feedback> +``` + 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..f4799f7b2c 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -12,15 +12,18 @@ [ -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/API \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ @@ -30,6 +33,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/tools/Makefile.devel b/dev/tools/Makefile.devel index 8dcc70cf7f..ffdb1bdca9 100644 --- a/dev/tools/Makefile.devel +++ b/dev/tools/Makefile.devel @@ -5,7 +5,7 @@ TOPDIR=. BASEDIR= -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel +SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API default: usage noargument diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a3d5cf5c12..6ae5125f6d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,6 +8,7 @@ (* Printers for the ocaml toplevel. *) +open API open Util open Pp open Names @@ -26,17 +27,17 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) +let _ = Detyping.set_detype_anonymous (fun ?loc _ -> 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 *) let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) (* name printers *) -let ppid id = pp (pr_id id) +let ppid id = pp (Id.print id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) @@ -59,20 +60,13 @@ let pprecarg = function str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) -let pprecarg = function - | Declarations.Norec -> str "Norec" - | Declarations.Mrec (mind,i) -> - str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" - | Declarations.Imbr (mind,i) -> - str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) - (* term printers *) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) -let ppconstr x = pp (Termops.print_constr x) +let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) +let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -85,26 +79,26 @@ let ppbigint n = pp (str (Bigint.to_string n));; let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset pr_id (Id.Set.elements l)) +let ppidset l = pp (prset Id.print (Id.Set.elements l)) let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" let pridmap pr l = - let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in + let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) let ppidmap pr l = pp (pridmap pr l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr c ++ + (Termops.print_constr (EConstr.of_constr c) ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr c ++ str">") ++ + Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () - else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) + else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) -let prididmap = pridmap (fun _ -> pr_id) -let ppididmap = ppidmap (fun _ -> pr_id) +let prididmap = pridmap (fun _ -> Id.print) +let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") @@ -138,15 +132,15 @@ let safe_pr_global = function int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") - | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") + | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) @@ -158,15 +152,15 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) -let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppmetas metas = pp(Termops.pr_metaset metas) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -177,14 +171,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) let pphintdb db = pp(Hints.pr_hint_db db) let ppproofview p = let gls,sigma = Proofview.proofview p in - pp(pr_enum Goal.pr_goal gls ++ fnl () ++ pr_evar_map (Some 1) sigma) + pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) @@ -200,7 +194,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) @@ -214,7 +209,7 @@ let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) -let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) +let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = @@ -233,7 +228,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) @@ -455,8 +450,6 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) - let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" @@ -500,9 +493,9 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Pcoq +open Grammar_API open Genarg -open Constrarg +open Stdarg open Egramml let _ = @@ -519,7 +512,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] let _ = try @@ -535,47 +528,47 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] (* Setting printer of unbound global reference *) open Names open Libnames -let encode_path loc prefix mpdir suffix id = +let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - Qualid (loc, make_qualid + Qualid (Loc.tag ?loc @@ make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) -let raw_string_of_ref loc _ = function +let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = repr_con cst in - encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id) + let (mp,dir,id) = Constant.repr3 cst in + encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = repr_mind kn in - encode_path loc "IND" (Some (mp,dir)) [Label.to_id id] + let (mp,dir,id) = MutInd.repr3 kn in + encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = repr_mind kn in - encode_path loc "CSTR" (Some (mp,dir)) + let (mp,dir,id) = MutInd.repr3 kn in + encode_path ?loc "CSTR" (Some (mp,dir)) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) | VarRef id -> - encode_path loc "SECVAR" None [] id + encode_path ?loc "SECVAR" None [] id -let short_string_of_ref loc _ = function - | VarRef id -> Ident (loc,id) - | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn))) +let short_string_of_ref ?loc _ = function + | VarRef id -> Ident (Loc.tag ?loc id) + | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> - encode_path loc "IND" None [Label.to_id (pi3 (repr_mind kn))] + encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - encode_path loc "CSTR" None - [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] + encode_path ?loc "CSTR" None + [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 64431ea161..fa2864cec9 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident}} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index afa94a63e0..be6b914b6b 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,3 +1,4 @@ +open API open Format open Term open Names |