aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh19
-rwxr-xr-xdev/ci/ci-basic-overlay.sh26
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
-rwxr-xr-xdev/ci/ci-coqprime.sh8
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh5
-rwxr-xr-xdev/ci/ci-rewriter.sh8
-rwxr-xr-xdev/ci/ci-sf.sh16
-rwxr-xr-xdev/ci/ci-tlc.sh8
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile8
-rw-r--r--dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh6
-rw-r--r--dev/doc/changes.md2
-rw-r--r--dev/doc/critical-bugs28
-rw-r--r--dev/dune-workspace.all2
-rwxr-xr-xdev/tools/make-changelog.sh18
-rwxr-xr-xdev/tools/update-compat.py165
-rw-r--r--dev/top_printers.ml54
-rw-r--r--dev/vm_printers.ml2
17 files changed, 199 insertions, 178 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 78c0b4b2c7..82cc7a7117 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1132,11 +1132,22 @@ function make_findlib {
function make_dune {
make_ocaml
- if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
+ if build_prep https://github.com/ocaml/dune/archive/ 2.0.0 tar.gz 1 dune-2.0.0 ; then
log2 make release
log2 make install
+ # Dune support libs, we don't install glob and action-plugin as
+ # they are not needed by Coq
+ logn dune-private-build dune build -p dune-private-libs @install
+ logn dune-private-install dune install dune-private-libs
+
+ logn dune-configurator-build dune build -p dune-configurator @install
+ logn dune-configurator-install dune install dune-configurator
+
+ logn dune-build-info dune build -p dune-build-info @install
+ logn dune-build-info dune install dune-build-info
+
build_post
fi
}
@@ -1191,7 +1202,8 @@ function make_ocaml_cairo2 {
log2 dune build cairo2.install
log2 dune install cairo2
- log2 dune clean
+ # See https://github.com/ocaml/dune/issues/2921
+ # log2 dune clean
build_post
fi
@@ -1216,7 +1228,8 @@ function make_lablgtk {
log2 dune build -p lablgtk3-sourceview3
log2 dune install lablgtk3-sourceview3
- log2 dune clean
+ # See https://github.com/ocaml/dune/issues/2921
+ # log2 dune clean
build_post
fi
}
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8db0087e3c..87122e0fb5 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -144,6 +144,13 @@
: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}"
########################################################################
+# rewriter
+########################################################################
+: "${rewriter_CI_REF:=master}"
+: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}"
+: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}"
+
+########################################################################
# fiat_parsers
########################################################################
: "${fiat_parsers_CI_REF:=master}"
@@ -179,17 +186,11 @@
: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}"
########################################################################
-# SF
-########################################################################
-: "${sf_lf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz}"
-: "${sf_plf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz}"
-: "${sf_vfa_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz}"
-
-########################################################################
# TLC
########################################################################
-: "${tlc_CI_REF:=master}"
-: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}"
+: "${tlc_CI_REF:=master-for-coq-ci}"
+: "${tlc_CI_GITURL:=https://github.com/charguer/tlc}"
+: "${tlc_CI_ARCHIVEURL:=${tlc_CI_GITURL}/archive}"
########################################################################
# Bignums
@@ -199,6 +200,13 @@
: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}"
########################################################################
+# coqprime
+########################################################################
+: "${coqprime_CI_REF:=master}"
+: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}"
+: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
+
+########################################################################
# bedrock2
########################################################################
: "${bedrock2_CI_REF:=master}"
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2ac78d3c2b..8570c34194 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download bedrock2
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install )
diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh
new file mode 100755
index 0000000000..a4fd296896
--- /dev/null
+++ b/dev/ci/ci-coqprime.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coqprime
+
+( cd "${CI_BUILD_DIR}/coqprime" && make && make install)
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index e8c8d22678..000c418137 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -10,8 +10,9 @@ git_download fiat_crypto
# building the executables.
# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
-fiat_crypto_CI_TARGETS1="c-files printlite lite"
-fiat_crypto_CI_TARGETS2="coq"
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
+fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
ulimit -s 32768 && \
diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh
new file mode 100755
index 0000000000..235482ffeb
--- /dev/null
+++ b/dev/ci/ci-rewriter.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download rewriter
+
+( cd "${CI_BUILD_DIR}/rewriter" && make && make install)
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 60436e672c..2b1d2298f2 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,10 +3,18 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1
-wget -qO- "${sf_lf_CI_TARURL}" | tar xvz
-wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
-wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
+CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
+data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+
+mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
+
+sf_lf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "lf.tgz") | .url')
+sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url')
+sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url')
+
+wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
+wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
+wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
( cd lf && make clean && make )
( cd plf && make clean && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
new file mode 100755
index 0000000000..9802fc4ae1
--- /dev/null
+++ b/dev/ci/ci-tlc.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download tlc
+
+( cd "${CI_BUILD_DIR}/tlc" && make && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 1cad46cd89..8907843b12 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-11-05-V01"
+# CACHEKEY: "bionic_coq-V2019-12-03-V81"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -8,7 +8,7 @@ ENV DEBIAN_FRONTEND="noninteractive"
RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
# Dependencies of the image, the test-suite and external projects
- m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
+ m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
# Dependencies of lablgtk (for CoqIDE)
libgtksourceview-3.0-dev \
# Dependencies of stdlib and sphinx doc
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
# Common OPAM packages.
# `num` does not have a version number as the right version to install varies
# with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \
CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
BASE_ONLY_OPAM="elpi.1.8.0"
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
# EDGE switch
ENV COMPILER_EDGE="4.09.0" \
COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
- BASE_OPAM_EDGE="dune-release.1.3.2"
+ BASE_OPAM_EDGE="dune-release.1.3.3"
# EDGE+flambda switch, we install CI_OPAM as to be able to use
# `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh
new file mode 100644
index 0000000000..e0d9dc6469
--- /dev/null
+++ b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11172" ] || [ "$CI_BRANCH" = "master+coercion-notation-interleaved-printing" ]; then
+
+ elpi_CI_REF=coq-master+mini-fix-mkGApp
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 8ab00c6fd8..7d394c3401 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,5 @@
+## Changes between Coq 8.11 and Coq 8.12
+
## Changes between Coq 8.10 and Coq 8.11
### ML API
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 0631b3ad59..67becb251a 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -120,7 +120,17 @@ Universes
risk: unlikely to be activated by chance (requires a plugin)
component: template polymorphism
- summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though)
+ summary: template polymorphism not collecting side constrains on the
+ universe level of a parameter; this is a general form of the
+ previous issue about template polymorphism exploiting other ways to
+ generate untracked constraints
+ introduced: morally at the introduction of template polymorphism, 23
+ May 2006, 9c2d70b, r8845, Herbelin
+ impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3,
+ V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory
+ also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found
+ there yet (an exploit using a plugin to force sharing of universe
+ level is in principle possible though)
impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
@@ -129,6 +139,22 @@ Universes
GH issue number: #9294
risk: moderate risk to be activated by chance
+ component: template polymorphism
+ summary: using the same universe in the parameters and the
+ constructor arguments of a template polymorphic inductive (using
+ named universes in modern Coq, or unification tricks in older Coq)
+ produces implicit equality constraints not caught by the previous
+ template polymorphism fix.
+ introduced: same as the previous template polymorphism bug, morally
+ from V8.1, first verified impacted version V8.5 (the universe
+ unification is sufficiently different in V8.4 to prevent our trick
+ from working)
+ fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert)
+ found by: Gilbert
+ exploit: test-suite/bugs/closed/bug_11039.v
+ GH issue number: #11039
+ risk: moderate risk (found by investigating #10504)
+
component: universe polymorphism, asynchronous proofs
summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 28e8773e25..49e338d0a5 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,4 +1,4 @@
-(lang dune 1.10)
+(lang dune 2.0)
; Add custom flags here. Default developer profile is `dev`
(context (opam (switch 4.05.0)))
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index dbb60359cb..e1aed4560d 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -3,7 +3,7 @@
printf "PR number? "
read -r PR
-printf "Where? (type a prefix)\n"
+printf "Category? (type a prefix)\n"
(cd doc/changelog && ls -d */)
read -r where
@@ -11,11 +11,25 @@ where="doc/changelog/$where"
if ! [ -d "$where" ]; then where=$(echo "$where"*); fi
where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
+printf "Type? (type first letter)\n"
+printf "[A]dded \t[C]hanged \t[D]eprecated \t[F]ixed \t[R]emoved\n"
+read -r type_first_letter
+
+case "$type_first_letter" in
+ [Aa]) type_full="Added";;
+ [Cc]) type_full="Changed";;
+ [Dd]) type_full="Deprecated";;
+ [Ff]) type_full="Fixed";;
+ [Rr]) type_full="Removed";;
+ *) printf "Invalid input!\n"
+ exit 1;;
+esac
+
# shellcheck disable=SC2016
# the ` are regular strings, this is intended
# use %s for the leading - to avoid looking like an option (not sure
# if necessary but doesn't hurt)
-printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where"
+printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,\n by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where"
printf "Name of created changelog file:\n"
printf "$where\n"
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index c7bb36b6d3..ddb0362186 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -1,6 +1,8 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
from __future__ import with_statement
+from __future__ import print_function
import os, re, sys, subprocess
+from io import open
# When passed `--release`, this script sets up Coq to support three
# `-compat` flag arguments. If executed manually, this would consist
@@ -13,10 +15,8 @@ import os, re, sys, subprocess
# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
# with the deleted file.
# - Remove any notations in the standard library which have `compat "U.U"`.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-# bumping all the version numbers by one, and update the interpretations
-# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+# by bumping all the version numbers by one.
#
# - Remove the file
# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
@@ -36,10 +36,8 @@ import os, re, sys, subprocess
# - Update
# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
# with the added file.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-# bumping all the version numbers by one, and update the interpretations
-# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+# by bumping all the version numbers by one.
# - Update the files
# [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
# [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
@@ -68,10 +66,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
RELEASE_NUMBER_OF_OLD_VERSIONS = 2
MASTER_NUMBER_OF_OLD_VERSIONS = 3
EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli')
-FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
-G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
@@ -84,17 +79,25 @@ BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *)
(* It is autogenerated by %s. *)
""" % os.path.relpath(os.path.realpath(__file__), ROOT_PATH)
+def get_file_lines(file_name):
+ with open(file_name, 'rb') as f:
+ lines = f.readlines()
+ return [line.decode('utf-8') for line in lines]
+
+def get_file(file_name):
+ return ''.join(get_file_lines(file_name))
+
def get_header():
- with open(HEADER_PATH, 'r') as f: return f.read()
+ return get_file(HEADER_PATH)
HEADER = get_header()
-def break_or_continue():
- msg = 'Press ENTER to continue, or Ctrl+C to break...'
- try:
- raw_input(msg)
- except NameError: # we must be running python3
- input(msg)
+def fatal_error(msg):
+ if hasattr(sys.stderr, 'buffer'):
+ sys.stderr.buffer.write(msg.encode("utf-8"))
+ else:
+ sys.stderr.write(msg.encode("utf-8"))
+ sys.exit(1)
def maybe_git_add(local_path, suggest_add=True, **args):
if args['git_add']:
@@ -114,11 +117,10 @@ def maybe_git_rm(local_path, **args):
def get_version(cur_version=None):
if cur_version is not None: return cur_version
- with open(CONFIGURE_PATH, 'r') as f:
- for line in f.readlines():
- found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
- if len(found) > 0:
- return found[0]
+ for line in get_file_lines(CONFIGURE_PATH):
+ found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+ if len(found) > 0:
+ return found[0]
raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
def compat_name_to_version_name(compat_file_name):
@@ -132,8 +134,7 @@ def version_name_to_compat_name(v, ext='.v'):
# returns (lines of compat files, lines of not compat files
def get_doc_index_lines():
- with open(DOC_INDEX_PATH, 'r') as f:
- lines = f.readlines()
+ lines = get_file_lines(DOC_INDEX_PATH)
return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
tuple(line for line in lines if 'theories/Compat/Coq' not in line))
@@ -183,7 +184,7 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
if contents is None or contents != new_contents:
if not assert_unchanged:
print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
- with open(path, 'w') as f:
+ with open(path, 'w', encoding='utf-8') as f:
f.write(new_contents)
maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args)
else:
@@ -226,8 +227,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args)
else:
# print('Checking %s...' % compat_file)
- with open(compat_path, 'r') as f:
- contents = f.read()
+ contents = get_file(compat_path)
header = HEADER + (EXTRA_HEADER % v)
if not contents.startswith(HEADER):
raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
@@ -241,118 +241,38 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
contents = contents.replace(header, '%s\n%s' % (header, line))
update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args)
-def update_compat_versions_type_line(new_versions, contents, relpath):
- compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current'])
- new_compat_line = 'type compat_version = %s' % compat_version_string
- new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE)
- if new_compat_line not in new_contents:
- raise Exception("Could not find 'type compat_version =' in %s" % relpath)
- return new_contents
-
-def update_version_compare(new_versions, contents, relpath):
- first_line = 'let version_compare v1 v2 = match v1, v2 with'
- new_lines = [first_line]
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | %s, %s -> 0' % (V, V))
- new_lines.append(' | %s, _ -> -1' % V)
- new_lines.append(' | _, %s -> 1' % V)
- new_lines.append(' | Current, Current -> 0')
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find version_compare in %s' % relpath)
- return new_contents
-
-def update_pr_version(new_versions, contents, relpath):
- first_line = 'let pr_version = function'
- new_lines = [first_line]
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | %s -> "%s"' % (V, v))
- new_lines.append(' | Current -> "current"')
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find pr_version in %s' % relpath)
- return new_contents
-
-def update_add_compat_require(new_versions, contents, relpath):
- first_line = 'let add_compat_require opts v ='
- new_lines = [first_line, ' match v with']
- for v in new_versions[:-1]:
- V = 'V%s_%s' % tuple(v.split('.'))
- new_lines.append(' | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext='')))
- new_lines.append(' | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext=''))
- new_lines = '\n'.join(new_lines)
- new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
- if new_lines not in new_contents:
- raise Exception('Could not find add_compat_require in %s' % relpath)
- return new_contents
-
-def update_parse_compat_version(new_versions, contents, relpath, **args):
+def update_get_compat_file(new_versions, contents, relpath):
line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current
- first_line = 'let parse_compat_version = let open Flags in function'
+ first_line = 'let get_compat_file = function'
split_contents = contents[contents.index(first_line):].split('\n')
while True:
cur_line = split_contents[:line_count][-1]
if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None:
break
- elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None:
+ elif re.match(r'^ \| "[0-9\.]*" -> "Coq.Compat.Coq[0-9]*"$', cur_line) is not None:
line_count += 1
else:
- raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
+ raise Exception('Could not recognize line %d of get_compat_file in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
old_function_lines = split_contents[:line_count]
all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines))
invalid_versions = tuple(i for i in all_versions if i not in new_versions)
new_function_lines = [first_line]
- for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))):
+ for v, V in reversed(list(zip(new_versions, ['"Coq.Compat.Coq%s%s"' % tuple(v.split('.')) for v in new_versions]))):
new_function_lines.append(' | "%s" -> %s' % (v, V))
new_function_lines.append(' | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions))
new_lines = '\n'.join(new_function_lines)
new_contents = contents.replace('\n'.join(old_function_lines), new_lines)
if new_lines not in new_contents:
- raise Exception('Could not find parse_compat_version in %s' % relpath)
+ raise Exception('Could not find get_compat_file in %s' % relpath)
return new_contents
-def check_no_old_versions(old_versions, new_versions, contents, relpath):
- for v in old_versions:
- if v not in new_versions:
- V = 'V%s_%s' % tuple(v.split('.'))
- if V in contents:
- raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
-
-def update_flags_mli(old_versions, new_versions, **args):
- with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
- new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
-
-def update_flags_ml(old_versions, new_versions, **args):
- with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
- new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
-
def update_coqargs_ml(old_versions, new_versions, **args):
- with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
- new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+ contents = get_file(COQARGS_ML_PATH)
+ new_contents = update_get_compat_file(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
-def update_g_vernac(old_versions, new_versions, **args):
- with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
- new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
- check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
- update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
-
def update_flags(old_versions, new_versions, **args):
- update_flags_mli(old_versions, new_versions, **args)
- update_flags_ml(old_versions, new_versions, **args)
update_coqargs_ml(old_versions, new_versions, **args)
- update_g_vernac(old_versions, new_versions, **args)
def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args):
assert(len(new_versions) == len(test_suite_paths))
@@ -361,7 +281,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
contents = None
suggest_add = False
if os.path.exists(path):
- with open(path, 'r') as f: contents = f.read()
+ contents = get_file(path)
else:
suggest_add = True
if '%s' in descr: descr = descr % v
@@ -376,7 +296,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
remove_if_exists(path, assert_unchanged=assert_unchanged, **args)
def update_doc_index(new_versions, **args):
- with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
+ contents = get_file(DOC_INDEX_PATH)
firstline = ' theories/Compat/AdmitAxiom.v'
new_contents = ''.join(DOC_INDEX_LINES)
if firstline not in new_contents:
@@ -386,7 +306,7 @@ def update_doc_index(new_versions, **args):
update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
def update_test_suite_run(**args):
- with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read()
+ contents = get_file(TEST_SUITE_RUN_PATH)
new_contents = r'''#!/usr/bin/env bash
# allow running this script from any directory by basing things on where the script lives
@@ -410,7 +330,7 @@ def update_compat_notations(old_versions, new_versions, **args):
for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
for fname in files:
if not fname.endswith('.v'): continue
- with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+ contents = get_file(os.path.join(root, fname))
new_contents = update_compat_notations_in(old_versions, new_versions, contents)
update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
@@ -435,9 +355,8 @@ def parse_args(argv):
'git_add': False,
}
if '--master' not in argv and '--release' not in argv:
- print(r'''WARNING: You should pass either --release (sometime before branching)
+ fatal_error(r'''ERROR: You should pass either --release (sometime before branching)
or --master (right after branching and updating the version number in version.ml)''')
- if '--assert-unchanged' not in args: break_or_continue()
for arg in argv[1:]:
if arg == '--assert-unchanged':
args['assert_unchanged'] = True
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ccb8658eee..f7f2bcdcff 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -143,9 +143,9 @@ let pP s = pp (hov 0 s)
let safe_pr_global = let open GlobRef in function
| ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
| IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
- int i ++ str ")")
+ int i ++ str ")")
| ConstructRef ((kn,i),j) -> pp (str "CONSTRUCTREF(" ++ MutInd.debug_print kn ++ str "," ++
- int i ++ str "," ++ int j ++ str ")")
+ int i ++ str "," ++ int j ++ str ")")
| VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
@@ -225,7 +225,7 @@ let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst 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 (UnivProblem.Set.pr c)
-let ppuniverse_context_future c =
+let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
@@ -327,9 +327,9 @@ let constr_display csr =
| Set -> "Set"
| Prop -> "Prop"
| Type u -> univ_display u;
- "Type("^(string_of_int !cnt)^")"
+ "Type("^(string_of_int !cnt)^")"
- and universes_display l =
+ and universes_display l =
Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
then (" "^i) else "")) (Instance.to_array l) ""
@@ -398,7 +398,7 @@ let print_pure_constr csr =
print_string "Constr(";
sp_display sp;
print_string ",";
- print_int i; print_string ","; print_int j;
+ print_int i; print_string ","; print_int j;
print_string ","; universes_display u;
print_string ")"
| Case (ci,p,c,bl) ->
@@ -418,12 +418,12 @@ let print_pure_constr csr =
open_vbox 0;
let print_fix () =
for k = 0 to (Array.length tl) - 1 do
- open_vbox 0;
- name_display lna.(k); print_string "/";
- print_int t.(k); print_cut(); print_string ":";
- box_display tl.(k) ; print_cut(); print_string ":=";
- box_display bl.(k); close_box ();
- print_cut()
+ open_vbox 0;
+ name_display lna.(k); print_string "/";
+ print_int t.(k); print_cut(); print_string ":";
+ box_display tl.(k) ; print_cut(); print_string ":=";
+ box_display bl.(k); close_box ();
+ print_cut()
done
in print_string"{"; print_fix(); print_string"}"
| CoFix(i,(lna,tl,bl)) ->
@@ -433,10 +433,10 @@ let print_pure_constr csr =
let print_fix () =
for k = 0 to (Array.length tl) - 1 do
open_vbox 1;
- name_display lna.(k); print_cut(); print_string ":";
- box_display tl.(k) ; print_cut(); print_string ":=";
- box_display bl.(k); close_box ();
- print_cut();
+ name_display lna.(k); print_cut(); print_string ":";
+ box_display tl.(k) ; print_cut(); print_string ":=";
+ box_display bl.(k); close_box ();
+ print_cut();
done
in print_string"{"; print_fix (); print_string"}"
| Int i ->
@@ -454,7 +454,7 @@ let print_pure_constr csr =
| Set -> print_string "Set"
| Prop -> print_string "Prop"
| Type u -> open_hbox();
- print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
+ print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
and name_display x = match x.binder_name with
| Name id -> print_string (Id.to_string id)
@@ -465,8 +465,8 @@ let print_pure_constr csr =
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
- | ("Coq"::_::l) -> l
- | l -> l
+ | ("Coq"::_::l) -> l
+ | l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
print_string (MutInd.debug_to_string sp)
and sp_con_display sp =
@@ -474,8 +474,8 @@ let print_pure_constr csr =
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
- | ("Coq"::_::l) -> l
- | l -> l
+ | ("Coq"::_::l) -> l
+ | l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
print_string (Constant.debug_to_string sp)
@@ -483,8 +483,8 @@ let print_pure_constr csr =
try
box_display csr; print_flush()
with e ->
- print_string (Printexc.to_string e);print_flush ();
- raise e
+ print_string (Printexc.to_string e);print_flush ();
+ raise e
let print_pure_econstr c = print_pure_constr EConstr.Unsafe.(to_constr c) ;;
@@ -568,12 +568,12 @@ let raw_string_of_ref ?loc _ = let open GlobRef in function
| IndRef (kn,i) ->
let (mp,id) = MutInd.repr2 kn in
encode_path ?loc "IND" (Some mp) [Label.to_id id]
- (Id.of_string ("_"^string_of_int i))
+ (Id.of_string ("_"^string_of_int i))
| ConstructRef ((kn,i),j) ->
let (mp,id) = MutInd.repr2 kn in
encode_path ?loc "CSTR" (Some mp)
- [Label.to_id id;Id.of_string ("_"^string_of_int i)]
- (Id.of_string ("_"^string_of_int j))
+ [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
@@ -589,7 +589,7 @@ let short_string_of_ref ?loc _ = let open GlobRef in function
[Label.to_id (MutInd.label 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
+(* Anticipate that printers can be used from ocamldebug and that
pretty-printer should not make calls to the global env since ocamldebug
runs in a different process and does not have the proper env at hand *)
let _ = Flags.in_debugger := true
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 11565b99eb..73cf1b0195 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -51,7 +51,7 @@ let rec ppzipper z =
let n = nargs args in
open_hbox ();
for i = 0 to n-2 do
- ppvalues (arg args i);print_string ";";print_space()
+ ppvalues (arg args i);print_string ";";print_space()
done;
if n-1 >= 0 then ppvalues (arg args (n-1));
close_box()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:52:03 +0000