Code Monkey home page Code Monkey logo

Comments (5)

vbgl avatar vbgl commented on July 18, 2024 1

Did you try to set mlPlugin = true;?

from aac-tactics.

CohenCyril avatar CohenCyril commented on July 18, 2024 1

@siraben according to release notes and opam metadata aac-tactics versions correspond one to one to coq versions, and there is not reason why aac-tactics-8.13 should succeed on anything else than coq-8.13.
Could you add a release of aac-tactics for each version of coq

from aac-tactics.

siraben avatar siraben commented on July 18, 2024

@CohenCyril @vbgl could you take a look?

from aac-tactics.

siraben avatar siraben commented on July 18, 2024

Thanks, the build still appears to fail on 8.11:

*** Warning: ra_common.ml already found in . (discarding ./ra_common.ml)

*** Warning: mrewrite.mlg already found in . (discarding ./mrewrite.mlg)

*** Warning: ra_fold.mlg already found in . (discarding ./ra_fold.mlg)

COQDEP mrewrite.mllib
COQDEP ra_fold.mllib
*** Warning: ra_common.mllib already found in . (discarding ./ra_common.mllib)

CAMLDEP kat_dec.ml
CAMLDEP ra_common.ml
CAMLDEP kat_reification.ml
CAMLDEP ra_reification.ml
CAMLDEP mrewrite.ml
CAMLDEP ra_fold.ml
*** Warning: mrewrite.mllib already found in . (discarding ./mrewrite.mllib)

*** Warning: ra_fold.mllib already found in . (discarding ./ra_fold.mllib)

COQC common.v
COQC comparisons.v
CAMLOPT -c  ra_common.ml
CAMLC -c kat_dec.mli
CAMLOPT -c  kat_dec.ml
File "ra_common.ml", line 61, characters 65-86:
61 |   lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.find_reference "RelationAlgebra.reification" dir s)))
                                                                      ^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Coqlib.find_reference
Please use Coqlib.lib_ref
CAMLOPT -a -o ra_common.cmxa
CAMLOPT -c  ra_fold.ml
File "ra_fold.mlg", line 89, characters 8-24:
Error: The constructor Case expects 4 argument(s),
       but is applied here to 5 argument(s)
make[1]: *** [Makefile.coq:626: ra_fold.cmx] Error 2
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile.coq:327: all] Error 2

but it succeeds on 8.13.

from aac-tactics.

siraben avatar siraben commented on July 18, 2024

Closing since resolved.

from aac-tactics.

Related Issues (20)

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.