Port to Coq 8.7 and template-coq v8.7 branch

[mattam82]

This is the port to Coq 8.7 and the current squiggle-eq and template-coq 8.7 branches. I needed admits in L4_5_to_L5.v due to changes in squiggle-eq apparently. Thanks to the new coq_makefile features I was able to remove an Obj.magic in CertiCoq's plugin, we really compile up to the interface of Template-Coq's produced OCaml Ast module now. The rest is:

• Require Import FunInd. in files that refer to functional induction.
• One rewrite * that works better, as expected.
• One removal of a unused intro pattern.
• The new syntax of universes in Template-Coq's AST, expected to stay that way.
• New universe_instance arguments in Template-Coq's AST for polymorphic constructs and declarations, ignored for now.

That was just a few hours of work :) The plugin works as expected.

[mattam82]

I made quite a few changes so that CertiCoq looks more like a regular Coq package that can be installed:

• Everything lives in the CertiCoq namespace now (required a few changes in L6 which already used fully qualified imports, other files are not affected because requiring Foo when the current directory is in namespace CertiCoq will happily resolve to CertiCoq.Foo).
• I moved the plugin/ stuff at the toplevel, so it becomes another target of the toplevel makefile, and the extraction fiddling is now putting files in plugin/extraction/*
• make install target will install both the .vo's for CertiCoq's compiler in user-contrib/CertiCoq and the plugin itself in user-contrib/CertiCoq/Plugin. After installation, one can hence use the plugin like this:

Require Import Arith.
From CertiCoq.Plugin Require Import CertiCoq.

Definition foo := 3 + 4.

CertiCoq Compile foo.

This all compiles with coq-template-coq.2.0~beta, coq-paramcoq-1.0.5, coq-squiggle-eq.1.0.3 and coq-ext-lib.0.9.7

@aa755 Could you test on your setup before we switch officially?

[aa755]

Sure. Will start the build right away.

[aa755]

make succeeds. But on make install, I get the following error:

Bad -I option: extraction: No such file or directory
COQDEP CertiCoq.v
Fatal error: exception Sys_error("extraction: No such file or directory")  
  COQC CertiCoq.v
File "./CertiCoq.v", line 4, characters 0-36:                                   Error:
File not found on loadpath : certicoq_plugin.cmxs

[mattam82]

Ok, I probably should have [mkdir plugin/extraction] somewhere. You do see the extracted .ml's in theories/Extraction after make right?

[mattam82]

Should be fixed now. You can try make install directly again.

[aa755]

Yes, it is fixed now. make install worked and so did Certicoq Compile foo.

[mattam82]

Cool!

…

On Sat, Feb 17, 2018 at 2:09 PM Abhishek Anand ***@***.***> wrote: Yes, it is fixed now. make install worked and so did Certicoq Compile foo. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#3 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARXYDEyDXBoN0ztG80Sr_IkfUIjc_ks5tVs-EgaJpZM4RyFe2> .

[aa755]

We are ready to move to 8.7, aren't we? Should we make 8.7 the default branch? or merge this PR?

[mattam82]

Cool, thanks for the merge @aa755 !