GitLab

Moreover, this commit also performs the emacs compilation at build time
rather than install time. It also uninstalls why3.elc systematically.

Piotr Trojanek authored Jul 03, 2015 and Guillaume Melquiond committed Jun 10, 2016

Use an optional 'words argument to regexp-opt instead of explicitly
surrounding the result with special chars.

When sessions are saved and then loaded from disk, goal identifiers are
properly qualified. This is not the case when goals are still in memory
due to reloading a file in the ide. So merging can get confused since
several goals potentially share the same base name.

The date at which the configure script was run does not carry much
information, so get rid of it.

The main issue is that both ocamlc and ocamlopt write a .cmi file when
there is no .mli file, so the .cmi file might end up being corrupted due
to concurrent accesses.

The ugly fix is to prevent ocamlopt from creating a .cmi file by lying to
it: ".mli files are no interface files, .but cmi files are". So ocamlopt
behaves as if there had been a .mli file in the first place and does not
try to produce a compiled interface from the .ml file. Note that we use
the .cmi file because it happens to have the same base name, but any other
file would have worked, e.g. the .dep file, since ocamlopt does not even
read the file to check that it is actually an interface file.

Since ocamlopt now believes that the .ml file has an interface, it needs a
compiled interface to check its signature against, so the .cmi file has to
be created beforehand. So the .cmx file is made to depend on the .cmi file
and the .cmi file on the .cmo file.

This might seem to add a dependency from the opt build on the byte build,
but since ocamldep already says that the tools depend on lib/why3/why3.cmo
due to the pack, this does not make the situation any worse.

Note that there is a single file for which the .cmi hack cannot be used:
src/tools/why3extract.ml. Indeed, if we lie to ocamlopt, it will try to
use lib/why3/why3extract.cmi as the compiled interface (?!) and thus fail
to compile src/tools/why3extract.ml, obviously. So the hack is disabled
for this file, which means that src/tools/why3extract.cmi could end up
being corrupted, but we do not care.

This reverts commit 6031de02.
Rationale: .cmxa files are not sufficient for cross-module optimizations.

Autoconf mandates an install-sh shell script. It can be installed using
"automake --add-missing" when working from the git repository.