aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-26extracting API for comparing universes of constants/inductives/constructorsbeta
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
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ↵coqbot-app[bot]
coercion not being used Reviewed-by: ejgallego
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-24Merge PR #13466: Fix linter: incorrect commit was picked in CIcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-24Merge PR #13455: Fix comparison of extracted array literalscoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
To tie the knot (since the evar depends on the evar type and the source of the evar type of the evar), we use an "update_source" function. An alternative could be to provide a function to build both an evar with its evar type directly in evd.ml...
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction ↵coqbot-app[bot]
of universes in "Context" Reviewed-by: SkySkimmer
2020-11-24Merge PR #13420: Modular printing algorithm for bench/render_results.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-24Merge PR #13411: Rename the confusing neutral annotation in CClosure.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-24Fix linter: incorrect commit was picked in CIGaëtan Gilbert
The bot merge was changed some time ago.
2020-11-24update default.nixEnrico Tassi
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 23:42:42 +0000