| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-06 | [stm] Switch to a functional API | Emilio Jesus Gallego Arias | |
| We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet. | |||
| 2017-10-06 | [stm] [flags] Move document mode flags to the STM. | Emilio Jesus Gallego Arias | |
| We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface. | |||
| 2017-10-06 | [coqtop] Don't reset coqinit internal variables after initialization. | Emilio Jesus Gallego Arias | |
| We remove `init_library_roots` as there is no point in resetting this internal variable. Its only user is `init_load_path` and this function is not meant (and is not) idempotent now. | |||
| 2017-10-06 | Merge PR #1127: Shorten the .gitattributes file. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵ | Maxime Dénès | |
| Compute plugin | |||
| 2017-10-06 | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | |
| "_something") | |||
| 2017-10-06 | Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵ | Maxime Dénès | |
| inductive definition) | |||
| 2017-10-06 | Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵ | Maxime Dénès | |
| BZ#4852) | |||
| 2017-10-06 | Merge PR #1128: GitLab CI: make all_stdlib.v in build job | Maxime Dénès | |
| 2017-10-06 | Merge PR #1130: Fix copyright info in reference manual. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1131: Clean-up xml protocol doc | Maxime Dénès | |
| 2017-10-06 | Merge PR #1129: 8.7+beta2 CHANGES | Maxime Dénès | |
| 2017-10-06 | Merge PR #1123: [ci] Remove deploy to GitHub of OS X package. | Maxime Dénès | |
| 2017-10-06 | Extract changes to the XML protocol from its doc | Théo Zimmermann | |
| 2017-10-06 | Make the XML protocol doc more version-independent | Théo Zimmermann | |
| 2017-10-06 | Fix copyright info in reference manual. | Théo Zimmermann | |
| Also simplifies the way it is presented (no need to be overly precise). | |||
| 2017-10-06 | 8.7+beta2 CHANGES | Théo Zimmermann | |
| 2017-10-05 | Merge PR #1069: Improve support for -w options | Maxime Dénès | |
| 2017-10-05 | Merge PR #1081: Mini fix at improving the cannot unify error message | Maxime Dénès | |
| 2017-10-05 | Fix typo in INSTALL | Maxime Dénès | |
| 2017-10-05 | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵ | Maxime Dénès | |
| to escape non-UTF-8 file names) | |||
| 2017-10-05 | Merge PR #1093: [doc] Update INSTALL to match reality. | Maxime Dénès | |
| 2017-10-05 | Merge PR #1107: Add coqwc tests to test suite | Maxime Dénès | |
| 2017-10-05 | GitLab CI: make all_stdlib.v in build job | Gaëtan Gilbert | |
| 2017-10-05 | Merge PR #1106: Fix beautifier | Maxime Dénès | |
| 2017-10-05 | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | |
| BZ#5757) | |||
| 2017-10-05 | Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵ | Maxime Dénès | |
| cleared context. | |||
| 2017-10-05 | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵ | Maxime Dénès | |
| coq_makefile are in sync (supersed #1039)… | |||
| 2017-10-05 | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | Maxime Dénès | |
| 2017-10-05 | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵ | Pierre Letouzey | |
| BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions). | |||
| 2017-10-05 | Shorten the .gitattributes file. | Théo Zimmermann | |
| .dir-locals.el can be useful for users of the tarballs as well, and TODO doesn't exist anymore. | |||
| 2017-10-05 | [pp] Minor optimization in `Pp.t` construction and gluing. | Emilio Jesus Gallego Arias | |
| The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans. | |||
| 2017-10-05 | [ci] Remove deploy to GitHub of OS X package. | Théo Zimmermann | |
| This is inconvenient because it can only be tested on tags and it didn't work for V8.7+beta1. | |||
| 2017-10-05 | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | |
| 2017-10-05 | Distinguishing pseudo-letters out of the set of unicode letters. | Hugo Herbelin | |
| This includes _ and insecable space which can be used in idents and this allows more precise heuristics. | |||
| 2017-10-05 | Fixing typos in comments of unicode.ml. | Hugo Herbelin | |
| 2017-10-05 | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition). | Hugo Herbelin | |
| 2017-10-04 | Merge PR #1006: fix: ssrmatching and primitive projections | Maxime Dénès | |
| 2017-10-04 | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | |
| 2017-10-04 | Extraction : minor support stuff for the new Extraction Compute plugin | Pierre Letouzey | |
| See https://github.com/letouzey/extraction-compute for more details | |||
| 2017-10-04 | Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677] | Maxime Dénès | |
| 2017-10-04 | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | |
| 2017-10-03 | add coqwc tests | Paul Steckler | |
| 2017-10-03 | fix compilation on OCaml < 4.04 | Enrico Tassi | |
| 2017-10-03 | Merge PR #1110: Mention requiring extraction/funind in CHANGES | Maxime Dénès | |
| 2017-10-03 | Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags. | Maxime Dénès | |
| 2017-10-03 | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links. | Maxime Dénès | |
| 2017-10-03 | Merge PR #1100: Avoid looping when searching for CoqProject. | Maxime Dénès | |
| 2017-10-03 | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵ | Maxime Dénès | |
| proof for coqwc | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |