aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/ci-basic-overlay.sh104
-rw-r--r--dev/ci/ci-common.sh45
-rwxr-xr-xdev/ci/ci-compcert.sh2
-rwxr-xr-xdev/ci/ci-iris-lambda-rust.sh4
-rw-r--r--dev/ci/user-overlays/06535-fix-push-rel-to-named.sh4
-rw-r--r--dev/ci/user-overlays/06686-ccnv-no-proj.sh4
-rw-r--r--dev/doc/COMPATIBILITY201
-rw-r--r--dev/doc/changes.md11
-rwxr-xr-xdev/lint-repository.sh13
-rwxr-xr-xdev/tools/check-eof-newline.sh19
-rwxr-xr-xdev/tools/merge-pr.sh20
-rwxr-xr-xdev/tools/should-check-whitespace.sh6
-rwxr-xr-xdev/tools/sudo-apt-get-update.sh4
-rw-r--r--dev/vm_printers.ml2
14 files changed, 336 insertions, 103 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 232b8a56e4..784da6f971 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -4,141 +4,143 @@
# Maybe we should just use Ruby to have real objects...
+# : "${foo:=bar}" sets foo to "bar" if it is unset or null
+
########################################################################
# MathComp
########################################################################
-: ${mathcomp_CI_BRANCH:=master}
-: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}
+: "${mathcomp_CI_BRANCH:=master}"
+: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
########################################################################
# UniMath
########################################################################
-: ${UniMath_CI_BRANCH:=master}
-: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
+: "${UniMath_CI_BRANCH:=master}"
+: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
########################################################################
# Unicoq + Metacoq
########################################################################
-: ${unicoq_CI_BRANCH:=master}
-: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}
+: "${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}
+: "${metacoq_CI_BRANCH:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
########################################################################
# Mathclasses + Corn
########################################################################
-: ${math_classes_CI_BRANCH:=master}
-: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+: "${math_classes_CI_BRANCH:=master}"
+: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}"
-: ${Corn_CI_BRANCH:=master}
-: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+: "${Corn_CI_BRANCH:=master}"
+: "${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}"
########################################################################
# Iris
########################################################################
-: ${stdpp_CI_BRANCH:=master}
-: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}
+: "${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}
+: "${Iris_CI_BRANCH:=master}"
+: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}"
-: ${lambdaRust_CI_BRANCH:=master}
-: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}
+: "${lambdaRust_CI_BRANCH:=master}"
+: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}"
########################################################################
# HoTT
########################################################################
-: ${HoTT_CI_BRANCH:=master}
-: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
+: "${HoTT_CI_BRANCH:=master}"
+: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}"
########################################################################
# Ltac2
########################################################################
-: ${ltac2_CI_BRANCH:=master}
-: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}
+: "${ltac2_CI_BRANCH:=master}"
+: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}"
########################################################################
# GeoCoq
########################################################################
-: ${GeoCoq_CI_BRANCH:=master}
-: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}
+: "${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}
+: "${Flocq_CI_BRANCH:=master}"
+: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}"
########################################################################
# Coquelicot
########################################################################
-: ${Coquelicot_CI_BRANCH:=master}
-: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
+: "${Coquelicot_CI_BRANCH:=master}"
+: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}"
########################################################################
# CompCert
########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: "${CompCert_CI_BRANCH:=master}"
+: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}"
########################################################################
# VST
########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: "${VST_CI_BRANCH:=master}"
+: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
########################################################################
# fiat_parsers
########################################################################
-: ${fiat_parsers_CI_BRANCH:=master}
-: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+: "${fiat_parsers_CI_BRANCH:=master}"
+: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}"
########################################################################
# fiat_crypto
########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+: "${fiat_crypto_CI_BRANCH:=master}"
+: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}"
########################################################################
# formal-topology
########################################################################
-: ${formal_topology_CI_BRANCH:=ci}
-: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
+: "${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}
+: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}"
+: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}"
########################################################################
# CoLoR
########################################################################
-: ${CoLoR_CI_BRANCH:=master}
-: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}
+: "${CoLoR_CI_BRANCH:=master}"
+: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}"
########################################################################
# SF
########################################################################
-: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}
-: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}
-: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}
+: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}"
+: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}"
+: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}"
########################################################################
# TLC
########################################################################
-: ${tlc_CI_BRANCH:=master}
-: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+: "${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}
+: "${bignums_CI_BRANCH:=master}"
+: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}"
########################################################################
# Equations
########################################################################
-: ${Equations_CI_BRANCH:=8.8+alpha}
-: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}
+: "${Equations_CI_BRANCH:=8.8+alpha}"
+: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 58c90ff11d..d7a356930e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,9 +2,13 @@
set -xe
+# default value for NJOBS
+: "${NJOBS:=1}"
+export NJOBS
+
if [ -n "${GITLAB_CI}" ];
then
- export COQBIN=`pwd`/_install_ci/bin
+ export COQBIN="$PWD/_install_ci/bin"
export CI_BRANCH="$CI_COMMIT_REF_NAME"
else
if [ -n "${TRAVIS}" ];
@@ -15,8 +19,10 @@ else
then
export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
export CI_BRANCH="$CIRCLE_BRANCH"
+ else # assume local
+ export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
fi
- export COQBIN=`pwd`/bin
+ export COQBIN="$PWD/bin"
fi
export PATH="$COQBIN:$PATH"
@@ -26,14 +32,16 @@ export COQBIN="$COQBIN/"
ls "$COQBIN"
# Where we clone and build external developments
-CI_BUILD_DIR=`pwd`/_build_ci
+CI_BUILD_DIR="$PWD/_build_ci"
-for overlay in ${ci_dir}/user-overlays/*.sh; do
- source ${overlay}
+# shellcheck source=ci-basic-overlay.sh
+source "${ci_dir}/ci-basic-overlay.sh"
+for overlay in "${ci_dir}"/user-overlays/*.sh; do
+ # shellcheck source=/dev/null
+ source "${overlay}"
done
-source ${ci_dir}/ci-basic-overlay.sh
-mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+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
@@ -46,15 +54,16 @@ git_checkout()
# 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'`" )
+ local _DEPTH=()
+ if [ -z "${4}" ]; then _DEPTH=(--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()
@@ -79,8 +88,8 @@ install_ssreflect()
{
echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
- checkout_mathcomp ${mathcomp_CI_DIR}
- ( cd ${mathcomp_CI_DIR}/mathcomp && \
+ checkout_mathcomp "${mathcomp_CI_DIR}"
+ ( cd "${mathcomp_CI_DIR}/mathcomp" && \
sed -i.bak '/ssrtest/d' Make && \
sed -i.bak '/odd_order/d' Make && \
sed -i.bak '/all\/all.v/d' Make && \
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fc3cef3426..6a0ce2aefa 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,7 +5,7 @@ source ${ci_dir}/ci-common.sh
CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
-opam install -j ${NJOBS} -y menhir
+opam install -j "$NJOBS" -y menhir
git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index cf24d202d9..267e13359b 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -34,8 +34,8 @@ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_UR
# Build std++
( cd ${stdpp_CI_DIR} && make && make install )
-# Build iris
-( cd ${Iris_CI_DIR} && make && make install )
+# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris
+( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install )
# Build lambdaRust
( cd ${lambdaRust_CI_DIR} && make && make install )
diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
new file mode 100644
index 0000000000..8a50fb1111
--- /dev/null
+++ b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then
+ Equations_CI_BRANCH=fix-6535
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
new file mode 100644
index 0000000000..3a3ab44e03
--- /dev/null
+++ b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then
+ Equations_CI_BRANCH=ccnv-fixes
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY
new file mode 100644
index 0000000000..a81afca32d
--- /dev/null
+++ b/dev/doc/COMPATIBILITY
@@ -0,0 +1,201 @@
+Note: this file isn't used anymore. Incompatibilities are documented
+as part of CHANGES.
+
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+ error rather than a warning when the superfluous name is already in
+ use. The easy fix is to remove the superfluous name.
+
+Potential sources of incompatibilities between Coq V8.5 and V8.6
+----------------------------------------------------------------
+
+Symptom: An obligation generated by Program or an abstracted subproof
+has different arguments.
+Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+and the subproof does not use the argument.
+Remedy:
+- Adapt the script.
+- Write an explicit lemma to prove the obligation/subproof and use it
+ instead (compatible with 8.4).
+- Unset the option for the program/proof the obligation/subproof originates
+ from.
+
+Symptom: In a goal, order of hypotheses, or absence of an equality of
+the form "x = t" or "t = x", or no unfolding of a local definition.
+Cause: This might be connected to a number of fixes in the tactic
+"subst". The former behavior can be reactivated by issuing "Unset
+Regular Subst Tactic".
+
+Potential sources of incompatibilities between Coq V8.4 and V8.5
+----------------------------------------------------------------
+
+* List of typical changes to be done to adapt files from Coq 8.4 *
+* to Coq 8.5 when not using compatibility option "-compat 8.4". *
+
+Symptom: "The reference omega was not found in the current environment".
+Cause: "Require Omega" does not import the tactic "omega" any more
+Possible solutions:
+- use "Require Import OmegaTactic" (not compatible with 8.4)
+- use "Require Import Omega" (compatible with 8.4)
+- add definition "Ltac omega := Coq.omega.Omega.omega."
+
+Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
+Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
+Possible solutions:
+- use "dintuition" instead; it is stronger than "intuition" and works
+ uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
+ (not compatible with 8.4)
+- do the script differently
+
+Symptom: The constructor foo (in type bar) expects n arguments.
+Cause: parameters must now be given in patterns
+Possible solutions:
+- use option "Set Asymmetric Patterns" (compatible with 8.4)
+- add "_" for the parameters (not compatible with 8.4)
+- turn the parameters into implicit arguments (compatible with 8.4)
+
+Symptom: "NPeano.Nat.foo" not existing anymore
+Possible solutions:
+- use "Nat.foo" instead
+
+Symptom: typing problems with proj1_sig or similar
+Cause: coercion from sig to sigT and similar coercions have been
+ removed so as to make the initial state easier to understand for
+ beginners
+Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
+
+* Other detailed changes *
+
+(see also file CHANGES)
+
+- options for *coq* compilation (see below for ocaml).
+
+** [-I foo] is now deprecated and will not add directory foo to the
+ coq load path (only for ocaml, see below). Just replace [-I foo] by
+ [-Q foo ""] in your project file and re-generate makefile. Or
+ perform the same operation directly in your makefile if you edit it
+ by hand.
+
+** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
+ load path.
+
+** Option [-I foo -as bar] is unchanged but discouraged unless you
+ compile ocaml code. Use -Q foo bar instead.
+
+ for more details: file CHANGES or section "Customization at launch
+ time" of the reference manual.
+
+- Command line options for ocaml Compilation of ocaml code (plugins)
+
+** [-I foo] is *not* deprecated to add foo to the ocaml load path.
+
+** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
+ the coq load path with logical name bar (shortcut for -I foo -Q foo
+ bar).
+
+ for more details: file CHANGES or section "Customization at launch
+ time" of the reference manual.
+
+- Universe Polymorphism.
+
+- Refinement, unification and tactics are now aware of universes,
+ resulting in more localized errors. Universe inconsistencies
+ should no more get raised at Qed time but during the proof.
+ Unification *always* produces well-typed substitutions, hence
+ some rare cases of unifications that succeeded while producing
+ ill-typed terms before will now fail.
+
+- The [change p with c] tactic semantics changed, now typechecking
+ [c] at each matching occurrence [t] of the pattern [p], and
+ converting [t] with [c].
+
+- Template polymorphic inductive types: the partial application
+ of a template polymorphic type (e.g. list) is not polymorphic.
+ An explicit parameter application (e.g [fun A => list A]) or
+ [apply (list _)] will result in a polymorphic instance.
+
+- The type inference algorithm now takes opacity of constants into
+ account. This may have effects on tactics using type inference
+ (e.g. induction). Extra "Transparent" might have to be added to
+ revert opacity of constants.
+
+Type classes.
+
+- When writing an Instance foo : Class A := {| proj := t |} (note the
+ vertical bars), support for typechecking the projections using the
+ type information and switching to proof mode is no longer available.
+ Use { } (without the vertical bars) instead.
+
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+ the global environment and inlined in the proof term when a proof
+ is ended with Qed. The behavior of 8.4 can be obtained by ending
+ proofs with "Qed exporting" or "Qed exporting ident, .., ident".
+
+Potential sources of incompatibilities between Coq V8.3 and V8.4
+----------------------------------------------------------------
+
+(see also file CHANGES)
+
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+ Several definitions have new names or are defined in modules of
+ different names, but a special care has been taken to have this
+ renaming transparent for the user thanks to compatibility notations.
+
+ However some definitions have changed, what might require some
+ adaptations. The most noticeable examples are:
+ - The "?=" notation which now bind to Pos.compare rather than former
+ Pcompare (now Pos.compare_cont).
+ - Changes in names may induce different automatically generated
+ names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+ - Z.add has a new definition, hence, applying "simpl" on subterms of
+ its body might give different results than before.
+ - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+ power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+ - The definition of functions over "vectors" (list of fixed length)
+ have changed.
+ - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+ - Less unfolding of fixpoints when applying destruct or inversion on
+ a fixpoint hiding an inductive type (add an extra call to simpl to
+ preserve compatibility).
+ - Less unexpected local definitions when applying "destruct"
+ (incompatibilities solvable by adapting name hypotheses).
+ - Tactic "apply" might succeed more often, e.g. by now solving
+ pattern-matching of the form ?f x y = g(x,y) (compatibility
+ ensured by using "Unset Tactic Pattern Unification"), but also
+ because it supports (full) betaiota (using "simple apply" might
+ then help).
+ - Tactic autorewrite does no longer instantiate pre-existing
+ existential variables.
+ - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+ - The command "Load" is now atomic for backtracking (use "Unset
+ Atomic Load" for compatibility).
+
+
+Incompatibilities beyond 8.4...
+
+- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
+ now "A -> (B <-> C)"
+
+- Tactics: tauto and intuition no longer accidentally destruct binary
+ connectives or records other than and, or, prod, sum, iff. In most
+ of cases, dtauto or dintuition, though stronger than 8.3 tauto and
+ 8.3 intuition will provide compatibility.
+
+- "Solve Obligations using" is now "Solve Obligations with".
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e616bd5663..aef62b0092 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -58,6 +58,17 @@ Declaration of printers for arguments used only in vernac command
happen. An alternative is to register the corresponding argument as
a value, using "Geninterp.register_val0 wit None".
+### STM API
+
+The STM API has seen a general overhaul. The main change is the
+introduction of a "Coq document" type, which all operations now take
+as a parameter. This effectively functionalize the STM API and will
+allow in the future to handle several documents simultaneously.
+
+The main remarkable point is that key implicit global parameters such
+as load-paths and required modules are now arguments to the document
+creation function. This helps enforcing some key invariants.
+
### XML IDE Protocol
- Before 8.8, `Query` only executed the first command present in the
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 87a8297461..ee9c8777a3 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,12 +9,12 @@
CODE=0
-if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
+if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
then
# skip PRs from before the linter existed
if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
then
- 2>&1 echo "Linting skipped: pull request older than the linter."
+ 1>&2 echo "Linting skipped: pull request older than the linter."
exit 0
fi
@@ -22,14 +22,13 @@ then
# can still check that they don't worsen.
CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
- MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
- dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1
+ MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD")
+ dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1
fi
# Check that the files with 'whitespace' gitattribute end in a newline.
# xargs exit status is 123 if any file failed the test
-find . "(" -path ./.git -prune ")" -type f \
--o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \
--print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1
+find . "(" -path ./.git -prune ")" -o -type f -print0 |
+ xargs -0 dev/tools/check-eof-newline.sh || CODE=1
exit $CODE
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 1c578c05ce..9e4c8661dc 100755
--- a/dev/tools/check-eof-newline.sh
+++ b/dev/tools/check-eof-newline.sh
@@ -1,9 +1,14 @@
#!/usr/bin/env bash
-if [ -z "$(tail -c 1 "$1")" ]
-then
- exit 0
-else
- echo "No newline at end of file $1!"
- exit 1
-fi
+CODE=0
+for f in "$@"; do
+ if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \
+ git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \
+ [ -n "$(tail -c 1 "$f")" ]
+ then
+ echo "No newline at end of file $f!"
+ CODE=1
+ fi
+done
+
+exit "$CODE"
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 0c4a79bfd3..9f24960fff 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -9,18 +9,18 @@ set -e
PR=$1
-CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD`
-REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote`
-git fetch $REMOTE refs/pull/$PR/head
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+git fetch "$REMOTE" "refs/pull/$PR/head"
API=https://api.github.com/repos/coq/coq
-BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
+BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
-COMMIT=`git rev-parse FETCH_HEAD`
-STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
+COMMIT=$(git rev-parse FETCH_HEAD)
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
-if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
echo "Wrong base branch"
read -p "Bypass? [y/N] " -n 1 -r
echo
@@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
fi
fi;
-if [ $STATUS != "success" ]; then
+if [ "$STATUS" != "success" ]; then
echo "CI status is \"$STATUS\""
read -p "Bypass? [y/N] " -n 1 -r
echo
@@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then
fi
fi;
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
# TODO: improve this check
-if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
echo "******************************************"
echo "** WARNING: does this PR have overlays? **"
echo "******************************************"
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
deleted file mode 100755
index d85d651070..0000000000
--- a/dev/tools/should-check-whitespace.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-
-# determine if a file has whitespace checking enabled in .gitattributes
-
-git ls-files --error-unmatch "$1" >/dev/null 2>&1 &&
-git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
new file mode 100755
index 0000000000..f8bf6bed41
--- /dev/null
+++ b/dev/tools/sudo-apt-get-update.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
+! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 8e43bf6ed0..f819d2e6a9 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -3,7 +3,7 @@ open Term
open Names
open Cbytecodes
open Cemitcodes
-open Vm
+open Vmvalues
let ppripos (ri,pos) =
(match ri with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:33:13 +0000