| Age | Commit message (Collapse) | Author |
|---|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
|
|
c.f. https://github.com/coq/coq/pull/11032#issue-335944369
Also, change the default from python2 to python3 for update-compat while
we're at it, and update file unicode handling accordingly.
(Note that this file still works with both python2 and python3.)
|
|
|
|
|
|
|
|
This removes spurious Ack-by lines
|
|
Fixes #10465
Following discussion we don't allow a generic `/usr/bin/python`
shebang anymore. We thus move all the scripts [but one] to python3,
and add python3 to the Azure base environment.
Unfortunately we still depend on python2 for the update-compat.py
script, see #10491
We thus have to complement #10467 adding python2 back to Nix,
until #10491 is fixed.
|
|
Remove other types of lines before copyright headers.
|
|
ml-style headers.
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
It now uses the origin/master branch rather than the master branch, thus
avoiding the need for local merges.
More importantly, it no longer creates a subshell in case of conflicts,
but instead gives control back to the user. Once conflicts are solved, it
suffices to relaunch the script (instead of exiting the subshell). The
reason is that, otherwise, there was no sane way of giving up a backport,
due to the infinite subshell loop.
|
|
PG would do it by default but since we override coq-prog-args it
doesn't.
|
|
Reviewed-by: ejgallego
|
|
|
|
shell buffer
Reviewed-by: ejgallego
|
|
|
|
It now removes the outdated `CompatOldOldFlag.v` file on `--release`,
and it now correctly updates `bug_9166.v` which seems to specifically be
about the compat flag behavior.
Additionally, it inserts an "autogenerated" notice at top of the two bug
files, and makes them read-only.
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
In response to review comments by Zimmi48
|
|
We now support --master and --release. On the master branch, we support
four compatibility versions, while on releases and release branches, we
support only three compatibility versions.
We also support --git-add to automatically run `git add` with new and
updated files, and to run `git rm` with deleted files.
|
|
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
It used to output duplicate trailers.
|
|
This produces a commit message like
~~~
Merge PR #9250: coqchk: fix check for kelim with functors
Reviewed-by: ppedrot
Ack-by: mattam92
~~~
|
|
|
|
|
|
|
|
This is very preliminary but you should get the idea. The script tries
to build contribs, then creates a branch and sets the remote properly
as to submit a PR.
Usage example:
```
./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi
```
This only works for contributions hosted in github for now.
|
|
|
|
|
|
|
|
Fixes #8621
|
|
compat updates to do as part of a release.
|
|
As requested in
https://github.com/coq/coq/issues/8311#issuecomment-415976318
the release process describes the steps to take.
All automatable steps are taken by the new script
dev/tools/update-compat.py
I've tried to make the script relatively easy to update if functions get
renamed or moved, but since it's doing unstructured source manipulation,
it is sort-of fragile.
We could plausibly add a file to the test-suite to ensure that we catch
script-breakage early, but this would require dropping compatibility
support much earlier in the development cycle (the compatibility changes
would have to come right when the new version is branched, rather than
shortly before the beta release).
|
|
This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
|
|
|
|
This way, when editors leave over temporary files from editing
user-overlays, we don't prevent commits unless they are added to git.
|
|
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|
|
|
[ci skip]
|
|
|
|
|
|
|
|
|
|
OpenBSD mktemp fails with an error otherwise.
|
|
```
$ dev/tools/check-owners-pr.sh 6809 --show-patterns --owner '@MSoegtropIMC'
remote: Counting objects: 93, done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 93 (delta 47), reused 50 (delta 47), pack-reused 43
Unpacking objects: 100% (93/93), done.
From github.com:coq/coq
* branch refs/pull/6809/head -> FETCH_HEAD
* branch master -> FETCH_HEAD
/dev/build/windows: @MSoegtropIMC
```
|
