aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.ml
Commit message (Collapse)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* Fix bug #5090: Effect of -Q depends on coqtop's current directory.Gravatar Pierre-Marie Pédrot2016-09-25
| | | | | | | This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It seems that the original motivation was to deactivate a warning when overriding the default loadpath binding of the current directory, but in the end it made it non-overridable.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
| | | | | | | | | | Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* | Move the From logic to Loadpath.expand_path.Gravatar Guillaume Melquiond2015-12-22
|/
* Unexport Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-30
|
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | | | | | | | | | 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.
* Make it possible for -R to override the existing implicit setting of a path.Gravatar Guillaume Melquiond2015-04-02
| | | | | Without this commit, passing "-R theories Coq" to "coqtop -nois" has no effect since "-Q theories Coq" has already been done implicitly.
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
|
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
|
* A more reasonable implementation of Loadpath.Gravatar Pierre-Marie Pédrot2015-03-31
| | | | | | | | The new behaviour is simple: either a path is in the loadpaths or it is not. No more wild expansions of paths! This should not affect -R and -Q, but it does change the semantics of -I -as. Still, there are no more users of it and it only does so in a subtle way.
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
| | | | | | | | 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.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
| | | | | | | | | | | | | | 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.
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
| | | | | | 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.
* Fix lookup of native files when option -R is missing.Gravatar Guillaume Melquiond2014-03-07
| | | | | | | | | | 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.*
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* code simplifications concerning SummaryGravatar letouzey2013-04-22
| | | | | | | | | | | | | | | - Most of the time, the table registered via Summary.declare_summary is just a single reference. A new function Summary.ref now allows to both declare this ref and register it to summary in one shot. - Clarifications concerning the role of [init_function]. For statically registered tables that don't need a special initializer, just do nothing there (see the new Summary.nop function). Beware: now that Summary exports a function named "ref", any code that do an "open Summary" will probably fail to compile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchronizing loadpath with the backtrack mechanism.Gravatar ppedrot2013-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7