aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh3
-rw-r--r--dev/ci/README-developers.md6
-rwxr-xr-xdev/ci/ci-wrapper.sh10
-rw-r--r--dev/doc/MERGING.md2
-rw-r--r--dev/doc/profiling.txt6
-rw-r--r--dev/doc/versions-history.tex2
-rwxr-xr-xdev/tools/merge-pr.sh2
-rwxr-xr-xdev/tools/update-compat.py38
8 files changed, 45 insertions, 24 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 07a13b8204..2e934ff0c0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -444,9 +444,6 @@ function load_overlay_data {
else
export CI_BRANCH=""
export CI_PULL_REQUEST=""
- # Used when building 8.8.0 with the latest scripts
- export TRAVIS_BRANCH=""
- export TRAVIS_PULL_REQUEST=""
fi
for overlay in /build/user-overlays/*.sh; do
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..10b4f9b044 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,12 @@ We are currently running tests on the following platforms:
`./configure`. It should allow complying with this discipline
without pain.
-- Travis CI is used to test the compilation of Coq and run the test-suite on
- macOS.
-
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
- Azure Pipelines is used to test the compilation of Coq and run the
- test-suite on Windows. It is expected to replace appveyor eventually.
+ test-suite on Windows and on macOS. It is expected to replace
+ appveyor eventually.
You can anticipate the results of most of these tests prior to submitting your
PR by running GitLab CI on your private branches. To do so follow these steps:
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 12a70176c2..9ca8f76054 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,13 +6,6 @@
set -eo pipefail
-function travis_fold {
- if [ -n "${TRAVIS}" ];
- then
- echo "travis_fold:$1:$2"
- fi
-}
-
CI_NAME="$1"
CI_SCRIPT="ci-${CI_NAME}.sh"
@@ -22,6 +15,5 @@ cd "${DIR}/../.."
export TIMED=1
"${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+echo 'Aggregating timing log...'
python ./tools/make-one-time-file.py time-of-build.log
-travis_fold 'end' 'coq.test.timing'
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 56fdab0c26..5705857d76 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the
When CI has a few failures which look spurious, restarting the corresponding
jobs is a good way of ensuring this was indeed the case.
-To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+To restart a job on AppVeyor, you should connect using your GitHub
account; being part of the Coq organization on GitHub should give you the
permission to do so.
To restart a job on GitLab CI, you should sign into GitLab (this can be done
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 29e87df6b8..8455d13377 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -10,7 +10,7 @@ In Coq source folder:
opam switch 4.05.0+trunk+fp
./configure -local -debug
make
-perf record -g bin/coqtop -compile file.v
+perf record -g bin/coqc file.v
perf report -g fractal,callee --no-children
To profile only part of a file, first load it using
@@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev
### For memory dump:
-CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+CAMLRUNPARAM=T,mj bin/coqc file.v
In another terminal:
@@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated.
### For complete memory graph:
-CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+CAMLRUNPARAM=T,gr bin/coqc file.v
In another terminal:
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 8f9c3171da..1c4913d201 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \
& & \feature{kernel-centric} architecture \\
& & more care for outside readers\\
& & (indentation, ocaml warning protection)\\
-Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\
+Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\
Coq V7.0beta2& released 2 February 2001\\
Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index a27dacc5a7..72e2930386 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -143,7 +143,7 @@ fi
# Sanity check: PR has an outdated version of CI
BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
-CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+CI_FILES=(".gitlab-ci.yml" "appveyor.yml")
if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
then
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index bde00a2f0d..ff9b32fe78 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -74,6 +74,7 @@ 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')
BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
+BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
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)
for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -81,6 +82,9 @@ TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-
# sanity check that we are where we think we are
assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools'))))
assert(os.path.exists(CONFIGURE_PATH))
+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_header():
with open(HEADER_PATH, 'r') as f: return f.read()
@@ -190,6 +194,15 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
print_diff(contents, new_contents)
raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
+def remove_if_exists(path, exn_string='%s exists when it should not!', assert_unchanged=False, **args):
+ if os.path.exists(path):
+ if not assert_unchanged:
+ print('Removing %s...' % os.path.relpath(path, ROOT_PATH))
+ os.remove(path)
+ maybe_git_rm(os.path.relpath(path, ROOT_PATH), **args)
+ else:
+ raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
+
def update_file(new_contents, path, **args):
update_if_changed(None, new_contents, path, **args)
@@ -343,7 +356,7 @@ def update_flags(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, **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))
assert(len(new_versions) == len(test_suite_descriptions))
for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
@@ -361,6 +374,8 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
lines.append('')
new_contents = '\n'.join(lines)
update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args)
+ for path in test_suite_outdated_paths:
+ 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()
@@ -391,12 +406,29 @@ def update_bug_4789(new_versions, **args):
# currently-supported compat version, which should never be the
# current version
with open(BUG_4798_PATH, 'r') as f: contents = f.read()
- new_contents = r"""Check match 2 with 0 => 0 | S n => n end.
+ new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end.
Notation "|" := 1 (compat "%s").
Check match 2 with 0 => 0 | S n => n end. (* fails *)
""" % new_versions[0]
update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
+def update_bug_9166(new_versions, **args):
+ # we always update this compat notation to oldest
+ # currently-supported compat version, which should never be the
+ # current version
+ with open(BUG_9166_PATH, 'r') as f: contents = f.read()
+ new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
+
+Notation bar := option (compat "%s").
+
+Definition foo (x: nat) : nat :=
+ match x with
+ | 0 => 0
+ | S bar => bar
+ end.
+""" % new_versions[0]
+ update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
+
def update_compat_notations_in(old_versions, new_versions, contents):
for v in old_versions:
if v not in new_versions:
@@ -469,6 +501,7 @@ if __name__ == '__main__':
new_versions = get_new_versions(known_versions, **args)
assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions'])
args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:])
+ args['test_suite_outdated_paths'] = tuple(TEST_SUITE_PATHS[:-args['number_of_compat_versions']])
args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:])
update_compat_files(known_versions, new_versions, **args)
update_flags(known_versions, new_versions, **args)
@@ -476,5 +509,6 @@ if __name__ == '__main__':
update_test_suite_run(**args)
update_doc_index(new_versions, **args)
update_bug_4789(new_versions, **args)
+ update_bug_9166(new_versions, **args)
update_compat_notations(known_versions, new_versions, **args)
display_git_grep(known_versions, new_versions)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:30:17 +0000