| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
| |
longer use camlp4.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| |
|
|
|
|
| |
This allows to share the test for possible relocalisation done in envars.ml.
|
|
|
|
|
|
|
|
|
|
| |
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?
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
This goes towards an approach where a local layout can be seen as an
installed layout.
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
Used to guess again the ocamlfind location at Coq's execution time.
An option to override the value (inferred at ./configure time) is available.
So, what is the point of guessing it? Either it stays there, or the
user is doing a hack, and has a flag to do it.
|
|
|
|
|
| |
This way a makefile can just iterate on this list, intead of
having a bunch of -I hardcoded in there by coq_makefile
|
|
|
|
| |
and avoid duplication
|
| |
|
|\ |
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
correct case on MacOS X whose file system is case-insensitive but
case-preserving (HFS+ configured in case-insensitive mode).
Generalized it to any case-preserving case-insensitive file system,
which makes it applicable to Windows with NTFS used in
case-insensitive mode but also to Linux when mounting a
case-insensitive file system.
Removed the blow-up of the patch, improved the core of the patch by
checking whether the case is correct only for the suffix part of the
file to be found (not for the part which corresponds to the path in
which where to look), and finally used a cache so that the effect of
the patch is not observable.
Note that the cache is implemented in a way not synchronous with
backtracking what implies e.g. that a file compiled in the middle of
an interactive session would not be found until Coq is restarted, even
by backtracking before the corresponding Require.
For history see commits
b712864e9cf499f1298c1aca1ad8a8b17e145079,
4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
69941d4e195650bf59285b897c14d6287defea0f
e7043eec55085f4101bfb126d8829de6f6086c5a.
as well as
https://coq.inria.fr/bugs/show_bug.cgi?id=2554
discussion on coq-club "8.5 and MathClasses" (May 2015)
discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015)
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files"
and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X."
This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.
Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.
|
| | |
|
|/
|
|
|
| |
Nothing is done for camlp4
There is an issue with computing camlbindir
|
|
|
|
|
| |
found in the file system have the expected lowercase/uppercase
spelling)
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Revised Coqtop.parse_args in a cleaner and lighter style
- Improved error message in case of argument parse failure:
* tell which option is expecting a related argument
* in case of unknown options, warn about them all at once
* do not hide the previous error messages by filling the
screen with usage(). Instead, suggest the use of --help.
- Specialized boolean config field Coq_config.arch_is_win32
- Faster Envars.coqlib, which is back to (unit->string), and
just access Flags.coqlib. Caveat: it must be initialized once
via Envars.set_coqlib
- Avoid keeping an opened channel to the "revision" file
- Direct load of theories/init/prelude.vo, no detour via Loadpath
Beware : ./configure must be runned after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16280 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Based on a patch by Pierre-Yves Strub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16124 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This correspond to ocaml4 warning 6
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Beautify.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16031 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Document interface file.
- Now export references to ocaml compilers used to compile Coq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16030 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
For starting a bare coqtop, the recommended option is now "-noinit"
that skips the load of Prelude.vo. Option "-nois" is kept for
compatibility, it is now an alias to "-noinit".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15434 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
|