aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-05-29Configuration with -local definitively seen as an installation layout like ↵Hugo Herbelin
others.
2017-05-29Using the same strategy in coqdoc than in coqtop to guess the coqlib.Hugo Herbelin
2017-05-29Relying on computation done in Envars to discover the installation directories.Hugo Herbelin
This allows to share the test for possible relocalisation done in envars.ml.
2017-05-29Generalizing to docdir and datadir the test for a relocated installation.Hugo Herbelin
Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links?
2017-05-29Exporting the suffixes needed to build coqlib, docdir, etc.Hugo Herbelin
This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given.
2017-05-29Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Hugo Herbelin
This goes towards an approach where a local layout can be seen as an installed layout.
2017-05-29Configure: viewing compilation in -local itself as an installation layout.Hugo Herbelin
Consequence: docdir is always defined, no more "" in external preferences for manual and stdlib when using coqide in -local mode.
2017-05-29Configuration: always giving a value to configdir and datadir.Hugo Herbelin
They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
2017-05-29More structure and more code factorization in building defaultHugo Herbelin
installation paths in unix or win32. There are two layouts (self-contained or unix-like) and we build absolute paths from them. Under unix, there is a fully relative layout (when user gives a prefix) and a standard semi-relative layout (where most file are under /usr/local with the absolute /etc/xdg/coq as an exception). I respected the existing semantics that under cygwin, the unix layout is the default one when prefix is not given, but the self-contained layout is the default one when a prefix is given.
2017-05-29Unifying the layout of installation directories.Hugo Herbelin
There seems to have been several bugs, when -prefix is given: - Under win32: "" instead of "lib" (presumably introduced in ab442aed8, 2006) - Under win32: datadir, mandir, docdir should presumably be in "share", "man", "doc", as given in default - Under non-win32: coqdoc files should be in latex subdir not emacs subdir
2017-05-29Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.Hugo Herbelin
2017-05-29Mini-renaming in configure.ml to avoid switching back and forth fromHugo Herbelin
"libdir" to "COQLIBINSTALL" then "libdir", then "coqlib". For the record, here is how installation options are named at the current time in the different places they are used (if any): Name in Name in Name in Name of option Name in Name of option config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep -------------------------------------------------------------------------------------------------------- COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib DOCDIR DOCDIR docdir -docdir docdir CONFIGDIR configdir -configdir DATADIR datadir -datadir BINDIR -bindir MANDIR -mandir EMACSLIB -emacslib COQDOCDIR -coqdocdir Note: in envars.ml, docdir and coqlib are recomputed
2017-05-29Dead code (xdg_config_dirs).Hugo Herbelin
2017-05-28Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Maxime Dénès
2017-05-28Merge PR#683: coq_makefile: build .cma for each .mlpackMaxime Dénès
2017-05-28Merge PR#684: Trunk+fix coq makefile test suite on nixosMaxime Dénès
2017-05-28Merge PR#681: Fix votour for safe strings & warningsMaxime Dénès
2017-05-28Merge PR#680: add Show test with -emacs flag for trunkMaxime Dénès
2017-05-28Merge PR#676: Primitive Ltac definitions for first and solveMaxime Dénès
2017-05-28Merge PR#658: [coqdoc] Add keywords in bug 2884.Maxime Dénès
2017-05-27[coqlib] Deprecate redundant Coqlib functions.Emilio Jesus Gallego Arias
We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
2017-05-27coq_makefile: build .cma for each .mlpackEnrico Tassi
It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-27Exporting a few primitive tacticals as named Ltac definitions.Pierre-Marie Pédrot
2017-05-27Merge PR#686: [travis] temporary UniMath overlayMaxime Dénès
2017-05-27[travis] temporary UniMath overlayMaxime Dénès
We are waiting for an upstream merge of a fix related to coq_makefile2.
2017-05-27Add execution permission to test-suite file.Théo Zimmermann
2017-05-27Use specific shell for more robustness.Théo Zimmermann
2017-05-27Fix test-suite/coq-makefile on NixOS.Théo Zimmermann
2017-05-26Merge pull request #7 from SkySkimmer/checker+fix_votourEmilio Jesús Gallego Arias
[checker] [votour] resolve warning 52 fragile constant pattern
2017-05-26[checker] [votour] resolve warning 52 fragile constant patternGaëtan Gilbert
Also stop using failwith for flow control in tuple_of_string.
2017-05-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Maxime Dénès
resolution trace
2017-05-26Merge PR#655: Extra functions exported in EConstrMaxime Dénès
2017-05-26[checker] Add bin/votour to the coqocaml target.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix/disable warnings.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix build with -safe-string (bug 5553)Emilio Jesus Gallego Arias
2017-05-25add Show test with -emacs flagPaul Steckler
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25Merge PR#402: Uniform attribute handling in interfacesMaxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24[location] Fix warnings.Emilio Jesus Gallego Arias
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24ROmega: division-aware ReflOmegaCore, allowing trace without termsPierre Letouzey
The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k.
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
2017-05-24coq_makefile: use -include rather than includeEnrico Tassi
This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this!
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 00:44:49 +0000