aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-11-23Adding overlay.Pierre-Marie Pédrot
2018-11-23Merge PR #9021: merge-pr: Improve overlay checkMaxime Dénès
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-21Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlibEnrico Tassi
2018-11-21Merge PR #8961: dune: link kernel in checker instead of copying filesPierre-Marie Pédrot
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps.
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2018-11-20Merge PR #8948: [dune] Some tweaks to docs.Théo Zimmermann
2018-11-20[dune] Only build printers when the ltac plugin is available.Emilio Jesus Gallego Arias
This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq.
2018-11-20gitlab: Install stdlib doc in build:baseGaëtan Gilbert
Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes.
2018-11-20Fix dune-dbg using checker/main -> checker/coqchkGaëtan Gilbert
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19Merge PR #9003: [vernacextend] Consolidate extension points APIPierre-Marie Pédrot
2018-11-19Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.Pierre-Marie Pédrot
2018-11-19Adding overlays.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
This is documented in dev/doc/changes.md.
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-18merge-pr: Improve overlay checkGaëtan Gilbert
2018-11-18Merge PR #9018: [devtools] Small script to setup overlays automaticallyGaëtan Gilbert
2018-11-17[devtools] Small script to setup overlays automaticallyEmilio Jesus Gallego Arias
This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now.
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
This is convenient as to have better automation.
2018-11-17[ci] Cleanup of old overlays.Emilio Jesus Gallego Arias
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
`CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913.
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR.
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-13Merge PR #8976: CoqHammer CIGaëtan Gilbert
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API.
2018-11-13Merge PR #8978: nix helpers for debugging external projects from CIEmilio Jesus Gallego Arias
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
Avoid downloading Coq.
2018-11-12CoqHammer CILukasz Czajka
2018-11-12Helpers for debugging external projects from CIVincent Laporte
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8949: Remove checker printersEmilio Jesus Gallego Arias
2018-11-09Adding an overlay for #8601.Pierre-Marie Pédrot
2018-11-08[dune] Some tweaks to docs.Emilio Jesus Gallego Arias
2018-11-08Remove checker printersGaëtan Gilbert
Now that the checker is using the regular kernel files it can also use the normal printers.
2018-11-08Merge PR #8944: Revert PR #8923 (require camlp5 >=7.06)Gaëtan Gilbert
2018-11-08Merge PR #8098: Update/improve two aspects of the merging process.Maxime Dénès
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
2018-11-07Bump up the minimal camlp5 version to 7.06.Pierre-Marie Pédrot
This is the first release that contains the type-safe grammar API.
2018-11-07Merge PR #8918: Fix overlays on Windows CIMichael Soegtrop
2018-11-07Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost)Emilio Jesus Gallego Arias
2018-11-07Merge PR #8773: [checker] Refactor by sharing code with the kernelPierre-Marie Pédrot
2018-11-06Update/improve two aspects of the merging process.Théo Zimmermann
Following discussion in #7042, we write down an advice to give time for last comments before merging potentially controversial PRs. We document a practice that is becoming standard in order to improve PR merging time: some other maintainer can self-assign if the main maintainer is not responding. Encourage component maintainers to announce when they won't be available. We document the practice of code owner teams. Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2018-11-06[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1Vincent Laporte
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update.
2018-11-06Fix overlays on Windows CIGaëtan Gilbert
"${foo+}" is always the empty string "${foo-}" is "$foo" when foo is set and empty string when it's unset.
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files.
2018-11-06Add overlay for EquationsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 02:33:08 +0000