| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
The same warning exists in ocamllibdep so I copied the change there.
Detecting when 2 paths are the same is approximate, eg ././a.ml and
a.ml are considered different. Implementing realpath probably isn't
worth doing for this warning.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_.
We take this constraint into account in tools manipulating Ocaml file
names.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
|
|
| |
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]
|
| |
|
|
|
|
|
| |
Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends
already on all the .cmx inside it, no need to state explicitely
that the .cmxs depends on these inner .cmx. Same thing concerning
.cmxs built out of a single .cmx.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For now, the pack name reuse the previous .cma name of the plugin,
(extraction_plugin, etc).
The earlier .mllib files in plugins are now named .mlpack.
They are also handled by bin/ocamllibdep, just as .mllib.
We've slightly modified ocamllibdep to help setting the -for-pack
options: in *.mlpack.d files, there are some extra variables such as
foo/bar_FORPACK := -for-pack Baz
when foo/bar.ml is mentioned in baz.mlpack.
When a plugin is calling a function from another plugin, the name
need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).
Btw, we discard the generated files plugins/*/*_mod.ml, they are
obsolete now, replaced by DECLARE PLUGIN.
Nota: there's a potential problem in the micromega directory,
some .ml files are linked both in micromega_plugin and in csdpcert.
And we now compile these files with a -for-pack, even if they are
not packed in the case of csdpcert. In practice, csdpcert seems
to work well, but we should verify with OCaml experts.
|
| | |
|
| | |
|
| |
|
Gaëtan Gilbert
Théo Zimmermann
Pierre-Marie Pédrot
Hugo Herbelin
Matej Košík
Gaëtan Gilbert
Pierre Letouzey
Guillaume Melquiond