| Age | Commit message (Collapse) | Author |
|---|
|
Contributors are *not* required to prepare all the patches by
themselves. They can request help from project authors, who should be
ready to take part in this.
Also, finish replacing "development" by the more appropriate word
"project".
|
|
Reviewed-by: maximedenes
|
|
|
|
* Add hyperlinks
|
|
Reviewed-by: ppedrot
|
|
Also, stop pinging when copying checklist to new issue.
|
|
|
|
This is necessary until we get of the voboot step.
See https://github.com/coq/coq/pull/11406#issuecomment-577261843 for
more details.
|
|
|
|
|
|
Latest build on SF is erroring due to:
```
"messages" : [ {
"type" : "error",
"message" : "This job has been blocked because no credits are available on your plan. Please upgrade to continue building.",
"reason" : "execution-authorization-failed"
} ],
```
we temporary pin to the last successful job that produced artifacts.
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
cons and nil
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
|
|
We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.
|
|
As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .
In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.
Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.
We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.
Closes #6446
Example with backtrace from https://github.com/coq/coq/issues/11366
Old:
```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
New:
```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
|
|
This brings dune at version 2.1.2
|
|
|
|
|
|
Reviewed-by: JasonGross
|
|
|
|
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.
|
|
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
Integrate merging doc in the main contributing document.
|
|
Reviewed-by: ejgallego
|
|
- remove manual flexlink circular dependency handling
- use standard configure process instead of hand made windows make files
- enable parallel build
- remove bootstrapping step (maybe should be there for release builds)
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
INSTALL.md
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
|
|
For now we don't enable it in any source file, neither on dune files.
`lint-repository` has been updated so it will check `dune build @fmt`
returns 0.
|
|
|
|
|
|
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
Reviewed-by: Zimmi48
|
|
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
