| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.
The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.
Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.
Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
This is done by adding a fourth type of loadpath, the ones that are
neither implicit nor root, for the subdirectories of a -Q root.
Note: this means that scanning for available directories is no longer done
on the fly for -Q, but once and for all, as with -R.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.
Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.
For the record, the command-line size mandated by Posix is 4KB.
|
| |
|
|
|
|
| |
This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.
|
| |
|
|
|
|
|
|
|
|
| |
Testcase:
mkdir a
echo "Definition t := O." > a/a.v
coqc -R a a a/a.v
echo "Require Import a.a. Definition u := t." > b.v
coqc -I . b.v
rm -rf a b.*
|
|
|
the interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Théo Zimmermann
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
ppedrot