aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)Gravatar Emilio Jesus Gallego Arias2018-04-26
|\
| * 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
| * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
|/ | | | | | | | | | | | | | | | | | | | | | | | We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
* Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)Gravatar Emilio Jesus Gallego Arias2018-03-31
|\
| * Linter: verify overlay extensions.Gravatar Gaëtan Gilbert2018-03-31
| |
| * pre-commit: verify user overlay extensions (must be .sh).Gravatar Gaëtan Gilbert2018-03-31
| | | | | | | | This has come up a couple times.
* | Remove outdated patch from ci-sfGravatar Jasper Hugunin2018-03-29
|/
* Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵Gravatar Maxime Dénès2018-03-26
|\ | | | | | | AppVeyor fail.
* \ Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Enrico Tassi2018-03-26
|\ \
* \ \ Merge PR #7029: improve merge-pr scriptGravatar Maxime Dénès2018-03-23
|\ \ \
| * | | improve merge-pr scriptGravatar Enrico Tassi2018-03-23
| | | | | | | | | | | | | | | | | | | | The script now performs many more checks and reports errors in a more intelligible way.
* | | | More precise wording about the merge process.Gravatar Maxime Dénès2018-03-23
| | | | | | | | | | | | | | | | | | | | In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.
* | | | Refine a bit the decentralized merging process.Gravatar Maxime Dénès2018-03-21
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make GitHub assign only principal maintainers as reviewers. This reduces the level of noise (PRs with 10 code owners), and makes it easy for the assignee to check if all reviews have been completed (all reviewers in the list have to approve the PR, which was not the case before if two reviewers were assigned for the same component). This change means that when a principal maintainer submits a patch touching the component they own, they should ask a review from the secondary maintainer.
* | | Describe new merging process.Gravatar Maxime Dénès2018-03-19
| | |
* | | [win] update bignums to tag V8.8+beta1Gravatar Enrico Tassi2018-03-15
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 00:26:53 +0000