Giter Club home page Giter Club logo

coq-ltac2-compiler's People

Contributors

skyskimmer avatar

Stargazers

avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar

coq-ltac2-compiler's Issues

Ahead of time compilation

Not sure how to handle this.

As long as the compiler is separate from the main ltac2 plugin we need to be able to compile files which did not load the compiler.

We could imagine having a separate executable (like coqnative), or add some Compile File command to the plugin.

The compilation results then need to be handled by the build / install system (provide some Makefile template to include in Makefile.local for coq_makefile users? what about dune?)

Then they need to be detected and loaded when executing ltac2 tactics.

Mutable definitions lead to dynlink errors

The README says mutable definitions are not compiled. IIUC everything should still work, it would just be "slower". Is that correct?

Here's my test case:

From Ltac2 Require Import Ltac2.
Ltac2 mutable mut : unit := ().
Ltac2 test () := match mut with () => () end.

From Ltac2Compiler Require Import Ltac2Compiler.
Ltac2 Compile test.
(*
Warning: Skipped compilation of mutable definitions mut [tac2compile-skipped-mutable,ltac2,default]

Dynlink error: execution of module initializers in the shared library failed: File "plugins/ltac2/tac2env.ml", line 79, characters 2-8: Assertion failed
*)

I am running 8.18.0.

I had mixed success with reproducing my original, much larger example. Ltac2 Compile would succeed if I did it in the same file where the mutable definition lives, but not if I ran it in another file. The example above replicates the error message but isn't derived from my actual example. I hope it's the same underlying issue.

OCaml does not support unicode binders?

Thanks for fixing #4 so quickly! I managed to compile quite a few functions already (so far with a 10% speedup in the one test file I am looking at) but I got stuck again at the next binder error:

File "/tmp/tac2compile_02742a/fdc8e1b.ml", line 2399, characters 30-31:
2399 |                         (let ฯ† =
                                     ^
Error: Illegal character (\134)

Compilation produces code in incorrect order

I've found a particularly confusing bug and it took me a while to minimize and reproduce. Luckily the effort paid off. I think the bug is in evaluation order but I can only reproduce it with Ltac2 externals that manipulate global state, not with Ltac2's own mutable references so I am not entirely sure how about what's happening.

Please have a look at https://github.com/Janno/ltac2-compiler-bug-repro. I've only tested the code with 8.18 but I hope it still works with master. dune build should build everything. I didn't manage to write a working _CoqProject file so stepping through it in emacs doesn't work.

The code exposes a OCaml reference to an integer that is incremented and decremented in a stack-like fashion (i.e. decrementing only works if the argument provided is the result of the last increment). The problem is in Ltac2 test2. In > [ ... | .. push ..], the push is executed before the tactic for the first subgoal is finished. This can be prevented by adding a printf before push, as is done in Ltac2 test1.

Assertion failed in `force_nontac_expr`

I am still trying to make progress on compiling our automation and managed to minimize another failure:

From Ltac2Compiler Require Import Ltac2Compiler.
Ltac2 Compile apply_cancelx_instance.
Ltac2 beta_iota :=
  let x := { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] } in x.
Ltac2 test () := Std.eval_lazy beta_iota.
Set Debug "backtrace".
Ltac2 Compile test.

The failure disappears when using

Ltac2 beta_iota :=
  { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] }.

Unfortunately the backtrace is just pure confusion:

Error: Anomaly "File "src/tac2compile.ml", line 624, characters 2-8: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Unicode.next_utf8 in file "clib/unicode.ml", line 162, characters 16-34
Called from Unicode.ident_refutation.aux in file "clib/unicode.ml", line 267, characters 26-39
Called from Unicode.ident_refutation in file "clib/unicode.ml", line 271, characters 16-21
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml" (inlined), line 212, characters 16-41
Called from Vernacinterp.interp.(fun) in file "vernac/vernacinterp.ml", line 226, characters 54-111
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from NewProfile.profile in file "lib/newProfile.ml" (inlined), line 151, characters 32-36
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml" (inlined), line 226, characters 15-115
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 226, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2185, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 965, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2327, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2424, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 79, characters 29-50
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 153, characters 6-46

Raised at Exninfo.iraise in file "clib/exninfo.ml" (inlined), line 79, characters 4-11
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 164, characters 4-34
Called from Util.try_finally in file "lib/util.ml" (inlined), line 140, characters 16-19
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 168, characters 2-166
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml" (inlined), line 144, characters 6-32
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 433, characters 17-62

I am working on a slightly adapted fork of the main branch to make it work in 8.18 so the line numbers could be a little off.

Incorrect compilation of Array.empty 

Require Import Ltac2Compiler.Ltac2Compiler.
From Ltac2 Require Import Array.
Ltac2 test () := Array.empty.
Ltac2 Eval Array.length (test ()).
Ltac2 Compile Array.empty.
Ltac2 Eval Array.length (test ()). (* Fails with anomaly in `Tac2ffi.to_array` *)

reported by @Janno

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.