Giter VIP home page Giter VIP logo

psmt2-frontend's People

Contributors

acoquereau avatar coquera avatar kit-ty-kate avatar mewmew avatar

Stargazers

avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar

Forkers

mewbak mewpull kit-ty-kate iguernl jamesjer halbaroth

psmt2-frontend's Issues

Change syntax for define-fun command

We should not be able to use type variable in the body (but we do) such as
(define-fun f (par (A) ((x A)) Bool) (exists ((y A)) (= x y)))

Use
(define-fun <fun name> (par (<type list>) (<typed var list>) <return type> <term> ))
instead of
(define-fun <fun name> (par (<type list>) (<typed var list>) <return type>) <term>)

DESTDIR=foo make install does not work

I've been trying to create an AUR package for psmt2-frontend for Arch Linux. However, I've not been able to set DESTDIR when invoking make install.

Got:

[u@x1 psmt2-frontend-0.1]$ export DESTDIR=/home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend
[u@x1 psmt2-frontend-0.1]$ make install
OCAMLFIND_DESTDIR=/usr/lib/ \
  ocamlfind install psmt2-frontend src/psmt2Frontend.* src/*.mli META
ocamlfind: Cannot mkdir /usr/lib/psmt2-frontend: Permission denied
make: *** [Makefile:121: install] Error 2

Expected:

[u@x1 psmt2-frontend-0.1]$ export DESTDIR=/home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/
[u@x1 psmt2-frontend-0.1]$ make install
OCAMLFIND_DESTDIR=/home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/ \
  ocamlfind install psmt2-frontend src/psmt2Frontend.* src/*.mli META
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/version.mli
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/smtlib_parser.mli
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/options.mli
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.o
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmxs
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmxa
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmx
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmt
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmo
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cmi
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.cma
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/psmt2Frontend.a
Installed /home/u/Desktop/ocaml-psmt2-frontend/pkg/psmt2-frontend/lib/psmt2-frontend/META

Trivial typo

Since psmt2-frontend is now a dep for alt-ergo, I'm packaging it for the Debian distribution.

The tools detected a typo:

--- psmt2-frontend.orig/src/lib/smtlib_typed_env.ml
+++ psmt2-frontend/src/lib/smtlib_typed_env.ml
@@ -327,7 +327,7 @@
     let cstrs = SMap.find symb.c env.funs in
     if (List.length cstrs > 1) then
       error (Typing_error
-               ("Constructor have mutliple signatures : " ^ symb.c)) symb.p;
+               ("Constructor have multiple signatures : " ^ symb.c)) symb.p;
     (try (List.hd cstrs).params with _e ->
        error (Typing_error ("Undefined Constructor : " ^ symb.c)) symb.p;)
   with Not_found ->

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.