| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
```
|
|
|
|
|
|
upper-case
At the moment, when one tries to add an Ocaml module to Coq code-base
which is composed just from upper-cases letters,
the compilation fails with an error:
File "......ml", line 1:
Error: Error while linking ...
Reference to undefined global `FOO'
This commit removes the restriction.
|
|
more uniform
|
|
|
|
|
|
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.
|
|
|
|
Deprecations which can't be fixed in 4.02.3 are locally wrapped with
[@@@ocaml.warning "-3"]. The only ones encountered are
- capitalize to capitalize_ascii and variants. Changing to ascii would
break coqdoc -latin1 and maybe other things though.
- external "noalloc" to external [@@noalloc]
|
|
|
|
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
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
|
|
|
|
|
|
This fixes bedrock and eliminates warnings.
Thanks Jason Gross for debugging this!
|
|
This makes the following work correctly:
make only TGTS="foo bar" -j2
note that
make foo bar -j2
is not doing what you think
|
|
|
|
|
|
Restores compatibility with 8.6
|
|
|
|
|
|
|
|
This enables one to have just one rule to compile .ml -> .cmx.
By using $(FOR_PACK) in such rule one passes to ocamlopt
-for-pack ModName only when necessary.
Before this coq_makefile had to generate 2 different rules, depending if
the module was mentioned in an .mlpack.
|
|
|
|
and avoid duplication
|
|
|
|
|
|
The .mli only acknowledges the current API. I'm not guilty your honor!
|
|
It has been deprecated for a while in favor of `Qed`.
|
|
|
|
We allow for a dynamic setting of the STM debug flag, and we print
some more information about the result of `process_transaction`.
We also fix a printing bug due to mixing `Printf` and `Format`, which
are not compatible.
|
|
Was introduced in 5268efdef, reverted then readded in 1be9c4d.
|
|
|
|
|
|
|
|
|
|
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
|
|
|
|
By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
|
|
In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
|
|
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
|
|
|
|
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
|
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
|
|
The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
|
|
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
