| Age | Commit message (Collapse) | Author |
|---|
|
called (fix #13849).
The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.
This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.
|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
Add headers to a few files which were missing them.
|
|
`Nativelib` currently assumes that objects are built in some
particular directories, but this is not true in some cases, for
example, when building with Dune.
We add a new option `-nI` to allow clients to specify the OCaml
include dirs.
|
|
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
|
|
Fixes #6699
|
|
|
|
This will allow to merge back `Names` with `API.Names`
|
|
|
|
|
|
|
|
Solves an efficiency problem in Makefiles generated by coq_makefile.
|
|
|
|
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
|
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.
|
|
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
