aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Gravatar Maxime Dénès2018-05-07
|\
* | [ci] Add ounit to the base Docker package set.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | This should help #6808.
* | Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CIGravatar Gaëtan Gilbert2018-05-06
|\ \
| * | [gitlab] [circleci] Use a Custom Docker Image as base CI setup.Gravatar Emilio Jesus Gallego Arias2018-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383
* | | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
|/ / | | | | | | | | | | | | | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
| * Fixes issue #7083 / Windows build: Unify build logging to console (for ↵Gravatar Michael Soegtrop2018-05-03
| | | | | | | | appveyor) and files
| * Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomlyGravatar Michael Soegtrop2018-05-03
|/
* Merge PR #7400: ci-vst.sh: use -o progsGravatar Emilio Jesus Gallego Arias2018-05-03
|\
* | [ci]: add pidetop (fix #7336)Gravatar Enrico Tassi2018-05-02
| |
| * ci-vst.sh: use -o progsGravatar Gaëtan Gilbert2018-05-01
|/ | | | | This is closer to what we mean than reproducing the default target without progs.
* [ci] Fix #7396: VST is brokenGravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | This is due to our CI script relying on their makefile internals, unfortunately we still have to do this to avoid timeouts.
* Merge PR #7351: Always print explanation for univ inconsistency, rm ↵Gravatar Emilio Jesus Gallego Arias2018-04-27
|\ | | | | | | Flags.univ_print
* \ Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)Gravatar Emilio Jesus Gallego Arias2018-04-26
|\ \
| | * Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
| * | updating CI for Mtac2Gravatar Beta Ziliani2018-04-25
| |/
* | Merge PR #7290: Update debugging.mdGravatar Hugo Herbelin2018-04-25
|\ \ | |/ |/|
* | [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
* | Merge PR #7152: [api] Remove dependency of library on Vernacexpr.Gravatar Pierre-Marie Pédrot2018-04-23
|\ \
* \ \ Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.Gravatar Pierre-Marie Pédrot2018-04-23
|\ \ \
* \ \ \ Merge PR #7320: [ci] Also make some display targets for fiat-cryptoGravatar Emilio Jesus Gallego Arias2018-04-21
|\ \ \ \
| * | | | [ci] Also make some display targets for fiat-cryptoGravatar Jason Gross2018-04-20
| | | | | | | | | | | | | | | | | | | | | | | | | This will catch things like https://github.com/coq/coq/pull/7025#issuecomment-381424489
* | | | | CI: add fcsl-pcmGravatar Anton Trunov2018-04-20
|/ / / /
* | | | Merge PR #7219: merge script support https + typos in docGravatar Maxime Dénès2018-04-19
|\ \ \ \
* | | | | CI: extract iris git version without using opamGravatar Ralf Jung2018-04-18
| | | | |
* | | | | fix iris-lambda-rust CIGravatar Ralf Jung2018-04-18
| | | | |
* | | | | Merge PR #7242: Update the CI branch for Equations.Gravatar Gaëtan Gilbert2018-04-17
|\ \ \ \ \
* | | | | | pre-commit : do not fail miserably if git config has `apply.whitespace = fix`Gravatar Pierre Letouzey2018-04-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Having `--whitespace=` on all `git apply` in this script should make it insensitive to user setup in `~/.gitconfig`, at least `[apply] whitespace = fix`. Note that even this way, this script remains hugely fragile and non mature, and would better *not* be set by default for everybody.
| | | | | * Update debugging.mdGravatar Jasper Hugunin2018-04-15
| |_|_|_|/ |/| | | | | | | | | This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655
| | | * | [doc] [engine] Document `abort_on_undefined_evars`.Gravatar Emilio Jesus Gallego Arias2018-04-15
| |_|/ / |/| | |
| * | | Update the CI branch for Equations.Gravatar Théo Zimmermann2018-04-13
| | | |
* | | | Overlay for econstr in Evd.Gravatar Gaëtan Gilbert2018-04-13
| | | |
* | | | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
|/ / / | | | | | | | | | | | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* | | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Gravatar Pierre-Marie Pédrot2018-04-13
|\ \ \ | | | | | | | | | | | | contains evars
| | * | merge script support https + typos in docGravatar Pierre Courtieu2018-04-11
| |/ / |/| |
* | | Merge script: adds a way for confirmation to expect a newline.Gravatar Théo Zimmermann2018-04-09
| | | | | | | | | | | | This fulfils Gaetan's wish.
* | | Add sanity check in merge script: local branch is up-to-date.Gravatar Théo Zimmermann2018-04-09
| | | | | | | | | | | | | | | | | | In case the local branch is ahead of upstream, we only print a warning because it could be that we are merging several PRs in a row.
* | | Document requirement to have git >= 2.7 to use the merge script.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | | | | | As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
* | | Merge script does not warn when the remote is set to HTTPS.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | | | | | This should solve Emilio's problem.
* | | Merge script: use fetch URL for the remote.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | | | | | In case the push URL has been overriden to make it fetch-only.
* | | Merge PR #6809: Improve shell scriptsGravatar Michael Soegtrop2018-04-08
|\ \ \
* \ \ \ Merge PR #6960: [api] Move some types to their proper module.Gravatar Pierre-Marie Pédrot2018-04-06
|\ \ \ \
* \ \ \ \ Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)Gravatar Enrico Tassi2018-04-06
|\ \ \ \ \
| | | | | * [api] Remove dependency of library on Vernacexpr.Gravatar Emilio Jesus Gallego Arias2018-04-06
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Morally, `library` should not depend on the vernacular definition. This will also create problems when trying to modularize the codebase due to the cycle [vernacs depend for example on constrexprs]. The fix is fortunately easy.
| | | * | Improve shell scriptsGravatar zapashcanon2018-04-05
| |_|/ / |/| | |
| * | | Fixes issue #7172 (don't include MinGW make in install)Gravatar Michael Soegtrop2018-04-05
| | | |
* | | | Add note for homebrew users.Gravatar Théo Zimmermann2018-04-05
| | | |
* | | | Some advice about merge script dependencies.Gravatar Théo Zimmermann2018-04-05
| | | | | | | | | | | | | | | | Including: how to create a GPG key.
* | | | Improve the MERGING doc.Gravatar Théo Zimmermann2018-04-05
|/ / / | | | | | | | | | In particular, describes what to do with overlays.
* | | merge-pr.sh: cache github API callsGravatar Gaëtan Gilbert2018-04-03
| | |
| * | [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
|/ / | | | | | | | | | | | | | | | | | | | | | | We solve some modularity and type duplication problems by moving types to a better place. In particular: - We move tactics types from `Misctypes` to `Tactics` as this is their proper module an single user [with LTAC]. - We deprecate aliases in `Tacexpr` to such tactic types. cc: #6512
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 19:19:48 +0000