aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-11-27Merge PR #13449: [RM] script to notify "platform" projects to tagcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Merge PR #13482: Improved error message on nested proofscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-11-27[RM] script to notify "platform" projects to tagEnrico Tassi
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
Reviewed-by: gares
2020-11-27Improved error message on nested proofsFabian Kunze
to include most common reason when this happens on accident
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to ↵Pierre-Marie Pédrot
check resolution of evars more incrementally Ack-by: SkySkimmer Reviewed-by: gares Ack-by: ppedrot
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Merge PR #13491: Reactivate test-suite on MacOS X, accidently merged in #13476coqbot-app[bot]
Reviewed-by: gares
2020-11-26Reactivate test-suite on MacOS X, accidently merged in #13476.Hugo Herbelin
2020-11-26Fixes #13456: regression where tactic exists started to check evars ↵Hugo Herbelin
incrementally. The regression was due to #12365. We fix it by postponing the evars check after the calls to the underlying constructor tactic, while retaining using information from the first instantiations to resolve the latter instantiations.
2020-11-26Merge PR #13467: [ci] add job for intervalcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: silene
2020-11-26[ci] interval, disable native-computeEnrico Tassi
2020-11-26[ci] coquelicot, depend on ssr properEnrico Tassi
2020-11-26[ci] avoid always rebuilding jobs that use remakeEnrico Tassi
2020-11-26[ci] separate oddorder and fourcolor from mathcompEnrico Tassi
In this way interval does not have to wait too much
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
2020-11-26Merge PR #13481: [ci] elpi 1.12coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-26Merge PR #13476: MacOS X install: accepting both dylib and so extensions for ↵coqbot-app[bot]
gtk im modules Reviewed-by: gares
2020-11-26[ci] bump elpi to 1.12.0Enrico Tassi
2020-11-26[ci] add job for intervalEnrico Tassi
2020-11-26[ci] coquelicot, run make installEnrico Tassi
2020-11-26Merge PR #13379: Add a new evar source to refer to evars which are types of ↵coqbot-app[bot]
evars Reviewed-by: SkySkimmer
2020-11-26Merge PR #13464: [CI] Compcert uses system libscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-11-25Merge PR #13447: Remove unused parsing codecoqbot-app[bot]
Reviewed-by: herbelin
2020-11-25tmp deactivation test-suiteHugo Herbelin
2020-11-25MacOS X install: accepting both dylib and so extensions for gtk immodules.Hugo Herbelin
This was changed from so to dylib in dd7c679cf6, but it seems to depend on versions of gtk. Accepting both seems ok, assuming that at least one will work.
2020-11-25[docker] don't install ocamlformatEnrico Tassi
2020-11-25[ci] make compcert use flocq and menhirEnrico Tassi
2020-11-25[ci] job for menhirEnrico Tassi
2020-11-25Merge PR #13228: [micromega] Performance of liaPierre-Marie Pédrot
Reviewed-by: ppedrot Ack-by: vbgl
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Overlays for #13415Gaëtan Gilbert
2020-11-25Changelog for #13415Gaëtan Gilbert
2020-11-25Add tests for #13303Gaëtan Gilbert
2020-11-25Clean UnivBinders testGaëtan Gilbert
- rename @{u} to @{uu} (u is the default name so using @{u} doesn't test as much as it should) - move part of the test using Require to end of the file (when quickly testing changes this allows to run most of the test without compiling the Require'd file)
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern.
2020-11-25Reserve "sort_expr" for uninterned universesGaëtan Gilbert
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
Reviewed-by: gares
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
Reviewed-by: vbgl
2020-11-25Merge PR #13343: Update syntax in auto.rst chaptercoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24[ci] variable CI_INSTALL_DIR to use with --prefixEnrico Tassi
2020-11-24Add a changelog.Pierre-Marie Pédrot
2020-11-24Keep accessed objects in memory in Persistent_cache.Pierre-Marie Pédrot
2020-11-24Regenerate the csdp cache for the test-suite.Pierre-Marie Pédrot
2020-11-24Alternative implementation of the Micromega persistent cache.Pierre-Marie Pédrot
Instead of loading the whole file in memory, we simply load an index table associating a file position to a key hash. Cache access is then performed on the fly by unmarshalling the data whose hash corresponds and checking key equality.
2020-11-24Preserve sharing in the Micromega cache.Pierre-Marie Pédrot
For some reason it was explicitly deactivated since the file was added, but I have no idea why. Unsetting sharing would lead to potential explosive memory consumption at unmarshalling time which is not worth the minimal cost it has at marshalling time.
2020-11-24Add an explicit signature to the MakeCache functor in Micromega.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:47:37 +0000