aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
AgeCommit message (Collapse)Author
2020-11-15[dune] [opam] Generate opam files automatically using Dune.Emilio Jesus Gallego Arias
- closes #12376 : dune version is now consistent as suggested - cc #12858 : coqide and coqide-server do no depend on ocamlfind when built this way. - closes #13372 : more precision in the license identifier
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-02Update screenshot of shield icon (shown in CONTRIBUTING).Théo Zimmermann
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-09Update dev/doc/critical-bugsPierre Roux
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-15Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-15Clarify release-process.mdEnrico Tassi
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-04-26Document the signing procedure of released binary packages.Pierre-Marie Pédrot
2020-04-15[dev] [doc] Changes.Emilio Jesus Gallego Arias
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility?
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-06Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rulesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-01[dune] [doc] Be more explicit coqtop dependenciesEmilio Jesus Gallego Arias
Fixes #11726
2020-02-29[dune] [ocamldebug] Improve ocamldebug rulesEmilio Jesus Gallego Arias
We provide the closure of the dependencies manually. This is still a hack, but not so bad given that the `source`'d files still do contain that duplication too. Dune should provide this functionality so we can replace both this rule and the source files. Actually, that's not hard to implement, `utop` already supports a printer attribute so these are loaded automatically, so the ocamldebug mode could do the same. Should fix #11716
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type.
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-14Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker ↵Théo Zimmermann
packaging Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-02-13Merge PR #11450: Publishing a new version on Zenodo: not a relevant step for ↵Emilio Jesus Gallego Arias
beta versions. Reviewed-by: ejgallego
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
- Add a `--fuzz` option to `make-both-single-timing-files.py` Passing `--fuzz=N` allows differences in character locations of up to `N` characters when matching lines in per-line timing diffs. The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`. See also the discussion at https://github.com/coq/coq/pull/11076#pullrequestreview-324791139 - Allow passing `--real` to per-file timing scripts and `--user` to per-line timing script. This allows easily comparing real times instead of user ones (or vice versa). - Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build - We also now use argparse rather than a hand-rolled argument parser; there were getting to be too many combinations of options. - Fix the ordering of columns in Coq's build system; this is the equivalent of #8167 for Coq's build system. Fixes #11301 Supersedes / closes #11022 Supersedes / closes #11230
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-01-28docs: Update release-process.md about opam/docker packagingErik Martin-Dorel
* Add hyperlinks
2020-01-28Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml'sPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-25Publishing a new version on Zenodo: not a relevant step for beta versions.Théo Zimmermann
Also, stop pinging when copying checklist to new issue.
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-21[xml-protocol doc] Fix link to vscoqRamkumar Ramachandra
2020-01-19Merge PR #11406: [dune] [dbg] Add support for coqtop in dune-dbgGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-19Merge PR #11214: Add a script to pin CI developments.Gaëtan Gilbert
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-01-19Removing text saying XML is future of PG, adding explicitly vscoq as a userHugo Herbelin
2020-01-17[dune] [dbg] Add support for coqtop in dune-dbgEmilio Jesus Gallego Arias
We also workaround problem #11405 , however, this should be reverted once the problem is fixed in OCaml upstream.
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
As suggested by Pierre-Marie Pédrot, this is a more conservative version of #8771 . In this commit, we replace Coq's custom backtrace type with OCaml `Printexc.raw_backtrace`; this seems to already give some improvements in terms of backtraces [see below] and removes quite a bit of code. Main difference in terms of API is that backtraces become now first-class in `Exninfo`, and we seek to consolidate thus the exception-related APIs in that module. We also fix a bug in `vernac.ml` where the backtrace captured was the one of `edit_at`. Closes #6446 Example with backtrace from https://github.com/coq/coq/issues/11366 Old: ``` raise @ file "stdlib.ml", line 33, characters 17-33 frame @ file "pretyping/coercion.ml", line 406, characters 24-68 frame @ file "list.ml", line 117, characters 24-34 frame @ file "pretyping/coercion.ml", line 393, characters 4-1004 frame @ file "pretyping/coercion.ml", line 450, characters 12-40 raise @ unknown frame @ file "pretyping/coercion.ml", line 464, characters 6-46 raise @ unknown frame @ file "pretyping/pretyping.ml", line 839, characters 33-95 frame @ file "pretyping/pretyping.ml", line 875, characters 50-94 frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81 frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71 frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48 frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49 frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ``` New: ``` Raised at file "stdlib.ml", line 33, characters 17-33 Called from file "pretyping/coercion.ml", line 406, characters 24-68 Called from file "list.ml", line 117, characters 24-34 Called from file "pretyping/coercion.ml", line 393, characters 4-1004 Called from file "pretyping/coercion.ml", line 450, characters 12-40 Called from file "pretyping/coercion.ml", line 464, characters 6-46 Called from file "pretyping/pretyping.ml", line 839, characters 33-95 Called from file "pretyping/pretyping.ml", line 875, characters 50-94 Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81 Called from file "pretyping/pretyping.ml", line 1294, characters 21-94 Called from file "pretyping/pretyping.ml", line 1342, characters 20-71 Called from file "vernac/vernacentries.ml", line 1579, characters 17-48 Called from file "vernac/vernacentries.ml", line 2215, characters 8-49 Called from file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ```
2020-01-03Merge PR #11295: Use code owner teams for every component.Maxime Dénès
Reviewed-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:02:53 +0000