| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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...
|
| |/
|
|
|
|
| |
Warnings are just too hard to see. Also there is no point keeping a
noop option except to point people at the replacement, which does not
require configure to succeed.
|
| | |
|
| |
|
|
|
|
|
|
| |
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
Some messages were sometimes not printed because of the missing flushes.
We use a generic combinator suggested by Emilio.
|
| | | |
|
| | | |
|
| |/
|
|
| |
In this way it is easy to support multiple defaults
|
| |\ |
|
| | |
| |
| |
| | |
longer use camlp4.
|
| |/
|
|
|
|
|
|
|
|
|
| |
The hook created checks to see if dev/tools/pre-commit exists, and, if
so, runs it. This way, we don't have to do any fancy logic to update
the git pre-commit hook. The configure script never overwrites an
existing precommit hook, so users can disable it by creating an empty
pre-commit hook.
The check for existence is so that if users check out an old version of
Coq, attempting to commit won't give an error about non-existent files.
|
| |\ |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
2.18.3
|
| | | | |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0
even for much newer versions. This makes building Coq on Ubuntu
impossible without modifying configure. This commit fixes that problem.
See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for
the upstream bug.
This closes #6585
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
Cygwin/Windows
|
| | |/ /
|/| |
| | |
| | | |
Closes #6509.
|
| | | |
| | |
| | |
| | | |
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
|
| | | |
| | |
| | |
| | |
| | | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| | |/ |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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].
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
| |
We require 4.02.3.
|
| |
|
|
|
| |
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
This seems a safe choice as of today, but more advanced users would
like to tweak it, or we could even refine it by a configure option if
desired.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
| |/
|
|
| |
Fixes BZ#5779
|
| |
|
|
|
|
| |
E.g. -safe-string is set by configure.ml and made available to
both make (via config/Makefile) and coq_makefile (via
config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
It is a valid git tag (unlike 8.7~alpha) and will be considered by most
tools as < 8.7.0 (unlike 8.7.0+alpha).
|
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Maxime Dénès
Enrico Tassi
Jim Fehrle
Jason Gross
Vadim Zaliva
Théo Zimmermann
Jacques-Pascal Deplaix
Vincent Laporte
Paul Steckler
Hugo Herbelin
Tej Chajed