CRGTCoq20090323

Presents : Hugo, Tom, Arnaud, Julien, Jean-Marc, Stéphane, Pierre, Bruno, Vincent

• Pierre has presented ocamlbuild and shown a demo of his experiments in replacing the present Makefile with this tool.

Organization:

• Ocamlbuild comes with ocaml since 3.10 (?) - one single .ml file for any platform - a specific _build dir for the dirty stuff : own files, myocamlbuild is the analogous to make, this executable compiles stuff before installation - philosophy : one sees this ml file as a script, which is fact "compiled" each time. Hence one gets more than a shell, ie. the whole power of ocaml... - take advantage of the ocaml libs (+ a C lib) automatically - rules are obtained by a system of tags (demo) - dynamic handling of dependency, no static graph built. (no .d file or equivalent), calling ocamldep for each .mlConclusions and observations :

• It's faster (~= 1minute for compiling coq sources).

• The "source" code is shorter.

• Compilation is less verbose : one state line + a log file

• For the time being, Pierre ports the "spirit of the makefile" a such but tags could make possible to get rid of .ml4 extensions and name every ml file with a .ml extension.

• not sure how to adapt the multiple Makefile glued together which is the situation today.

• mltop.ml4 is more complicated and needs some hack because of the different compiled file you want to produce according to native / bytecode.

• It's work in progress : a matter of time to add all the rules. - Status of parallelism is still unclear. - This may be not subsume all the Makefile : for instance installation

• |/!/| : no backward compatibility with < 3.9

• Jean-Marc has received the server dedicated to multi-platform benchmarks via virtualization (xen). He is about to move everything (in particular the web page) to this server and to use it for Coq benchmark. This server is located at the server room in the Lix.

• The web server is called isis, but is behind the lix server hence accessible through http://www.lix.polytechnique.fr/coq. One needs a lix account to log in using ssh, otherwise http.

• Wiki will be at http://www.lix.polytechnique.fr/coqorico. - Summary of benchmarks will be at http://www.lix.polytechnique.fr/coq/bench - There will be a mysql database (for the drupal webpages), on a separated server for backup issues.

• Move should be completed approximately within two weeks - The most complicated to move the coq-club archive.

• Pierre : It would be nice to test ocamlbuild on the multiple architectures.

• Hugo makes some general remarks :

• configure should give more info (version of labelgtk, but not necessarily of gtk, ...), needed for bug reports.

• discussion about labelgtk : what information do we need to identify the class of architectures (+libs) that determines a specific behaviour of coqide

• Are we ready for a 8.1pl5? : only a few fixes and backward compatibility things is needed

• Shall we plan a 8.3 release in autumn ? : delay between 8.1 and 8.2 was much too long because of type classes/setoid rw but also due to a lot of bugfix. Hugo suggests that three moth before (end of summer) we freeze and only correct bugs considered critical. Pierre & Bruno : may be should we try to make a list, even unformal of the wanted features for the release 8.3 ?

• And what about libs?

  Pierre : what about move std lib to user contrib, to maintain compatibility?

  Hugo : does this mean putting version numbers on libraries?

  Bruno : pb of the reflexive tactics containing ml code, how to synchronize?

  Hugo (half provocative) : can we renounce to std lib and replace it with a pool of plugins possibly non inter-compatible, but with compatible subgraphs.

  Arnaud : as soon as you provide the tools to install the stuff...

  Vincent says he is working with Sylvain Legal to adapt a Cabal like tool to deal with Coq module dependencies.

  Pierre : which plugins do we want to be launched with coqtop ? CC, firstorder seem ok but what about others others becoming available at Require Import (extraction, dp, gappa). Other tactics have an unclear status like subtac or function.

  Hugo thinks that we don't have to be regressive with respect to the current state.

  Pierre points that with the plugin architecture, it is only a matter of Require. He asks developers to ensure that the new features they introduces become available through a Require Import. He also points the 'noinput' state to get a plain neat coqtop without any plugin nor lib.

  Bruno points that for instance tauto is in the main tactic bunch.

  Pierre asks what people think about a - warn-error option (any warning becoming an error stopping compilation)? No disagreement.