aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/mltop.ml
Commit message (Collapse)AuthorAge
* [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files *) coq_path : Names.DirPath.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = | VoPath of vo_path_spec | MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed.
* [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | | | | | | | | In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
* Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ | | | | | | to escape non-UTF-8 file names)
* | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| | | | | | | | | | | | | | | | | | | | | | An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info`
| * A possible fix for BZ#5715 (escape non-utf8 win32 file names).Gravatar Hugo Herbelin2017-09-13
|/ | | | | | | | | | | | | | | | | | | | On Win32, Sys.readdir translates the file names to the charset of the local "code page", which may be not compatible with utf8. Warnings referring to these names can be generated. These warnings may be sent to CoqIDE. To ensure a utf8 compliant communication, we escape non-utf8 file names under win32. In the CoqIDE/Coq communication, Glib.IO.read_chars expects an utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in conversion input". This fixes bug #5715 (Hangul characters not recognized in file names) but this does not solve the case of an operating system mounting a file system with a different coding convention than the default one, i.e. unicode using "Normalization Form Canonical Decomposition" in UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux, (non-normalized?) UTF-16 for NTFS on Windows.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [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.
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.