| Age | Commit message (Collapse) | Author |
|---|
|
This removes a use of internal obligation data `prg_poly` and a couple
of duplicate lines.
|
|
|
|
Not necessary anymore after the merge of obligation declaration into
the main path.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: ejgallego
Reviewed-by: erikmd
|
|
The main reason for this change is to reduce the number of places
where the Coq version is hardcoded.
But moreover, I don't see why that wouldn't work since dev is
precisely the version that is defined in the opam files.
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
|
|
|
|
|
|
This seems like a recurring pattern, and IMO makes a bit better API.
We also remove `merge_universe_subst` as it is not needed so far, as
we were creating stale `evar_map`s just for this purpose.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
|
|
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.
Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
This is needed for the case the sources are set to read-only mode, for
example when using Dune >= 2.5 [needed for the global cache support]
Fixes #12264
Co-authored-by: Ignat Insarov <kindaro@gmail.com>
|
|
Reviewed-by: ejgallego
|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
|
|
from ssreflect
Reviewed-by: Zimmi48
Ack-by: gares
|
|
|
|
This is akin to what we do for Gitlab.
|
|
Reviewed-by: ejgallego
|
|
but ssrsearch is not loaded.
Fixes #12338
|
|
|
|
cf "If this is implemented, long names might cause a printing
problem:" in #11852
|
|
reductions
Reviewed-by: JasonGross
Ack-by: Zimmi48
|
|
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.
|
|
|
|
Since `ocaml_pwd.ml` was added this unquoted glob would be expanded by
the shell before being passed to `find`.
|
|
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
introduced in #11756
Reviewed-by: Zimmi48
|
|
|
|
- use a different mirror for main cygwin archive
- (always) publish build log as artifact
- fix call to dune makefiles
- we do just build Coq for now, as:
+ dune is rebuilding Coq to run the test-suite, this needs move
investigation.
+ the test suite seems to take long and it times-out on Win.
|
|
This reverts commit 646a12b2f4660d6e9d5a812febdccab44221d1f0.
|
|
Analysis by Jason Gross:
> The previous semantics was to reset the file offset to 0 during the
> unlock operation, unless it fails, in which case you'd roll back the
> file offset to it's present position (and very dubiously not report
> any issues). The new semantics say to always roll the file offset
> back to it's initial position, meaning that the position is at the
> end of the file after unlocking. As far as I can tell, this results
> in appending marshelled blobs to the cache file on every call to
> add, rather than overwriting the cache file with the marshelled blob
> of the updated table. Presumably unmarshelling the concatenation of
> marshelled data can result in segfaults somehow? This also explains
> why the bug only shows up sometimes; you need to get the system into
> a state where it writes to the cache in a way that concatenates
> blobs in the right way, but once you have such a cache you'll
> segfault every time you read from it.
>
> I think we should probably assert false in the with block, or just
> remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html
> doesn't say anything about lockf erroring on unlocking). If we start
> seeing errors, we can turn it into a warning.
Closes: #12072
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
