[WIP] Change build system

[Gbury]

Switch to manual makefiles to ocp-build, and use ocp-autoconf. At the same time, perform a big cleanup of Makefiles (effectively, all the makefiles of next have been removed, and a new makefile written).

Remaining TODOS:

• build plugins
• install plugins
• add tests/non-regression rules to makefiles
• add archi Makefile target
• add public-release Makefile target

Still WIP, not ready to be merged.

[Gbury]

This should be reviewable. The build system now uses dune.
The archi target has been removed because it is surprisingly difficult to adapt to a build system.

[iguerNL]

It seems that the branch still has conflicts with next

[bobot]

What was the rational for not moving to ocp-build but to dune?

The sources/configure part about prefix/libdir/sharedir should soon not be needed. The checking of the presence of dune will of course stay, but it would be a good idea that dune give ways to simplify this part.

[Gbury]

Note that originally, I tried ocp-build, but later switched to dune. This was for the following reason:

• ocp-build only supports packs, and not prefixed libraries
• in case of packs, ocp-build is not currently able to build documentation.

About the prefix/libdir/sharedir: it is sort of necessary (at least part of it) because these values are used in lib/util/config.ml and are used for alt-ergo to print these directories when invoked with the correct command line option (the -where option). While this option could be removed, alt-ergo still search plugins in the pluginsdir directory, so one cannot get rid of this easily.

[bobot]

While this option could be removed, alt-ergo still search plugins in the pluginsdir directory, so one cannot get rid of this easily.

The goal is not to remove these variables but that dune support them out of the box, so that dune install works out of the box too. And that these variable could be used in dune files for generating config.ml files too.

How do you want to support plugins? For Frama-C, I'm defining plugins as an usual public library stanza just with the convention that they start with the same prefix frama-c-plugin-. Then I use findlib.dynload to do the loading.

[Gbury]

It would be great if dune was in charge of generating the config.ml file, however, I could not find how to do that in the current dune docs: there seems to be some support for substitution variables/watermaks (such as %%VERSION%%), but the docs don't mention that we have access to variables for libdir, bindir and so on...

Currently, as far as I understand, plugins in alt-ergo are simply seen as an archive file (either .cma or .cmxs), rather than a proper ocaml lib. Thus for now, they're are built as private libraries, and I added an install stanza to install the relevant .cma/.cmxs file, but using findlib.dynload would probably be much cleaner (cc @OCamlPro-Iguernlala ?).

[bobot]

the docs don't mention that we have access to variables for libdir, bindir and so on

I was not clear, it is not yet done, ocaml/dune#1579, but should be soon or at least the use cases supported in another way. It would also allow to ask the final binary to be relocatable.

but using findlib.dynload would probably be much cleaner

The advantage is to allow other people to easily create plugins.

[iguerNL]

I'm not expert of dune and/or findlib. But if using findlib.dynload would be cleaner, why not !

[Gbury]

Rebased and ready to be reviewed.
I'll try and add the archi target soon.

[Gbury]

All comments fixed, ^^

[Gbury]

Rebased (correctly this time).

[ACoquereau]

Can we have/need a link for plugins in sources/ ?

[Gbury]

Are plugins sufficiently frequently used to need symlinks ?

[iguerNL]

make AB-Why3 doesn't work

[iguerNL]

make lib, make gen not working

make clean does not remove generated file config.ml

[Gbury]

Typo fixed.
Currently make distclean remove the generated files. However, note that because Makefile includes Makefile.config which is generated together with config.ml by the configure script, any invocation to make (including make clean) will re-generate config.ml if needed, so I'm not sure what good it is to remove it with clean.

[iguerNL]

• add old compilations flags if they are not set by dune:

LIGHT_OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g $(WARNINGS) -inline 100 $(INCLUDES)

• enable some optimizations:

OFLAGS = $(LIGHT_BFLAGS) -O3 -unbox-closures -for-pack AltErgoLib

• enable warnings of Makefile.users, and add others as TODOs (in a comment):

WARNINGS= -w +A-45-27-4-9-44-32-48-41-6-22

# xxxx: Warning 22: user warnings
# x6 : Warning 60: unused module MyNums. ==> pb with recursive modules

# x623: Warning 27: unused variable binders
# x619: Warning 4 : this pattern-matching is fragile.
# x291: Warning 9 : the following labels are not bound in this record pattern:
# x161: Warning 44: this open statement shadows the value identifier = (which is later used)
# x134: Warning 32: unused value take_max.
# x37 : Warning 48: implicit elimination of optional argument ?kind
# x35 : Warning 41: Other belongs to several types: abstract Sig.lit_origin
# x26 : Warning 6 : label is_le was omitted in the application of this function.

• remove all .merlin files

• rename "dolmen" in toplevel file "dune-project"

[iguerNL]

almost OK.

• remove -annot flag
• make sure that every commit compiles (to easy, for instance, git bisect)

[iguerNL]

Hop ! big change !