aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | | | | The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
| * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* | Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | | | | | | | | This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
* | Export the various option localities in the API.Gravatar Pierre-Marie Pédrot2018-03-09
|/ | | | This prevents relying on an underspecified bool option argument.
* Use a proper warning when a summary is captured out of module scope.Gravatar Vincent Laporte2018-03-07
|
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
| | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
| | | | | This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1.
* Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
|
* Merge PR #6469: No universe constraints in Let definitionsGravatar Maxime Dénès2017-12-22
|\
* \ Merge PR #6449: Let definitions must not contain side-effects when reaching ↵Gravatar Maxime Dénès2017-12-20
|\ \ | | | | | | | | | the kernel.
| | * Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
| | | | | | | | | | | | | | | | | | We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions.
| | * Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
| |/ | | | | | | This allows to statically ensure well-formedness properties.
* | Merge PR #6284: Warning for absolute name masking (deprecated, should become ↵Gravatar Maxime Dénès2017-12-18
|\ \ | | | | | | | | | an error)
| | * Let definitions must not contain side-effects when reaching the kernel.Gravatar Pierre-Marie Pédrot2017-12-16
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Let definitions have the same behaviour if they are ended with a Qed or a Defined command, i.e. they are treated as if they were transparent. Indeed, it doesn't make sense for them to be opaque as they are going to be expanded away at the end of the section. For an unknown reason, handling of side-effects in Let definitions considers them as if they were opaque, i.e. the effects are inlined in the definition. This discrepancy has bad consequences in the kernel, where one is forced to juggle with universe constraints generated by polymorphic Let definitions. As a first phase of cleaning, we simply enforce by typing that Let definitions should be purified before reaching the kernel. This has the intended side-effect to make side-effects persistent in Let definitions, as if they were indeed truly transparent.
* | Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6275: [summary] Allow typed projections from global state.Gravatar Maxime Dénès2017-12-12
|\ \ \
* | | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | |
| * | | [summary] Adapt STM to the new Summary API.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | | | | | | | | | | | | | We need to a partial restore. I think that we could design a better API, but further work on the toplevel state should improve it progressively.
| * | | [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
| * | [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
* | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
|/ / | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* | Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \
| | * Warning for absolute name masking (making it deprecated, should becomeGravatar Matthieu Sozeau2017-11-30
| | | | | | | | | | | | an error)
| * | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |/ | | | | | | | | | | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
* / [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
|/ | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | Note the problem with `create_evar_defs`.
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Gravatar Maxime Dénès2017-11-13
|\ \
* | | [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
| | |
| | * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| |/ | | | | | | We do up to `Term` which is the main bulk of the changes.
| * [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/ | | | This will allow to merge back `Names` with `API.Names`
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | This is a first step towards some of the solutions proposed in #6008.
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | 4.02.3 has been the minimal OCaml version for a while now.
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
* Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\
* | [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
| | | | | | | | | | For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
* | Removing now useless former fix to #3333 (check valid module names).Gravatar Hugo Herbelin2017-09-12
|/ | | | | | The fix is not anymore needed after Id.of_string was made strict (5b218f87). This allows to support the whole official syntax of identifiers and not just the alpha-numerical ones (without quote).
* Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\
* \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \
| | * Canonically renaming fold_map into fold_left_map in library Name.Gravatar Hugo Herbelin2017-08-29
| |/ |/| | | | | Also adding fold_right_map by consistency.
* | Print names of all open blocksGravatar Tej Chajed2017-08-06
| | | | | | | | Fixes bug 5597.