| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It seems this passed under my radar, but the change of implementation of the
safe demarshaller introduced by native integers and floating point numbers is
dangerous.
For floats, it makes the demarshaller depend on float kernel representation.
This is just an alias to the standard OCaml float type, so this is currently
not problematic, but this makes the code fragile if ever we decide to change
it there. This would trigger unsound object casts without any complaint from
the type-checker. Furthermore, having such a low-level library depend on
the kernel library sounds like a anti-feature to me.
For native integers, the situation is direr. The demarshaller turns
unconditionally 64-bits integers into their Int63 representation, which
depends on the architecture. This means that when parsing vo files from
a architecture where these types are not the same, we are guaranteed to get
into unsound casts. Some of them *might* get caught by the value
representation checker, yet it is a footgun. The demarshaller should only
deal with OCaml representations and not try to mess with Coq specific
data types, otherwise we are going to face desynchronization and thus
unsound casts.
|
|
Ack-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
|
|
Reviewed-by: ppedrot
|
|
- Warn in some places where {x:T} is not assumed to occur (e.g. in
argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.
We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
|
|
This moves the encoding of "n" as "arg_n" closer to the user interface level.
Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
|
|
doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst
OK, thanks.
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
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.
|
|
doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
This is incorrect and has created some problems. We also remove
unneeded `dynlink` dep.
Closes #11217
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Reviewed-by: gares
|
|
The missing dependency impacted the algorithm for detecting default
clauses.
|
|
If these files are present in the latex directory, "make refman-pdf"
may fail to generate CoqRefMan.pdf.
|
|
|
|
Reviewed-by: gares
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
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>
|
|
in order to make builds reproducible.
See https://reproducible-builds.org/ for why this is good
and https://reproducible-builds.org/specs/source-date-epoch/
for the definition of this variable.
Fixes #11037
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
It seems we need to pass the token to the actual artifact download.
|
|
|
|
|
|
|
|
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
|
|
|
|
|
|
|
|
|
