| Age | Commit message (Collapse) | Author |
|---|
|
Cf. #12049.
|
|
Reviewed-by: JasonGross
|
|
Fix #11967
|
|
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but
only the non-ignored files will be affected.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
|
|
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>
|
|
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
|
|
|
|
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.
|
