Please add SNARK

[nilqed]

Please add SNARK.
Url: https://github.com/nilqed/SNARK
License: MPL 1.1
Tested in local-project with SBCL 1.2.16 (GNU/Linux x86_64) and CLISP 2.48 (win32).

SNARK, SRI's New Automated Reasoning Kit, is a theorem prover intended for
applications in artificial intelligence and software engineering. SNARK is
geared toward dealing with large sets of assertions; it can be specialized
with strategic controls that tune its performance; and it has facilities
for integrating special-purpose reasoning procedures with general-purpose
inference.

Thx :)

[quicklisp]

Does not build for me. SBCL's type inferencer is flagging an operation with a fatal warning:

; file: /home/quicklisp/quicklisp-controller/dist/build-cache/snark/12854d211af9c7470311710fa66f86168115a860/snark-20160301-git/src/unify-bag.lisp
; in: DEFUN UNIFY-BAG-BASIS
;     (+ 1
;        (LOOP SNARK::FOR SNARK::K SNARK::BELOW SNARK::NXCOEFS
;              WHEN (PLUSP (SVREF SNARK::XSOL SNARK::K)) RETURN SNARK::K))
; 
; note: deleting unreachable code

;     (+ 1
;        (LOOP SNARK::FOR SNARK::K SNARK::BELOW SNARK::NYCOEFS
;              WHEN (PLUSP (SVREF SNARK::YSOL SNARK::K)) RETURN SNARK::K))
; 
; note: deleting unreachable code

;     (+ 1
;        (LOOP SNARK::FOR SNARK::K SNARK::BELOW SNARK::NXCOEFS
;              WHEN (PLUSP (SVREF SNARK::XSOL SNARK::K)) RETURN SNARK::K))
; 
; caught WARNING:
;   Constant NIL conflicts with its asserted type NUMBER.
;   See also:
;     The SBCL Manual, Node "Handling of Types"

;     (+ 1
;        (LOOP SNARK::FOR SNARK::K SNARK::BELOW SNARK::NYCOEFS
;              WHEN (PLUSP (SVREF SNARK::YSOL SNARK::K)) RETURN SNARK::K))
; 
; caught WARNING:
;   Constant NIL conflicts with its asserted type NUMBER.
;   See also:
;     The SBCL Manual, Node "Handling of Types"
Unhandled UIOP/LISP-BUILD:COMPILE-FILE-ERROR in thread #<SB-THREAD:THREAD "main thread" RUNNING {1003D9D6A3}>: COMPILE-FILE-ERROR while compiling #<CL-SOURCE-FILE "snark-implementation" "unify-bag">

The fatal part is "Constant NIL conflicts with its asserted type NUMBER".

http://report.quicklisp.org/2016-03-01/failure-report/snark.html#snark has more context of the build log.

[quicklisp]

I'm using SBCL 1.3.2+.

[nilqed]

Sorry about that. Yet, I'm rather surprised as there weren't any
problems up to now. Moreover, I couldn't reproduce the error with SBCL
1.3.3 (neither on Win7 nor on Ubuntu 14.04), however, I found the error
message in
https://groups.google.com/forum/#!msg/comp.lang.lisp/z5_QsksOeYY/sSF0qWcr5poJ
which might give reason to suppose a SBCL specific (version) issue.

I'm going to try your combination SBCL 1.3.2.136-7c6bbaa / ASDF 3.1.5 in
a docker image, but this might take a while ;)

Many thanks and
best regards
Kurt

C:\Users\scios\quicklisp\local-projects>git clone
https://github.com/nilqed/SNARK.git

Cloning into 'SNARK'...
remote: Counting objects: 159, done.
remote: Compressing objects: 100% (128/128), done.
remote: Total 159 (delta 30), reused 159 (delta 30), pack-reused
0Receiving obje

Receiving objects: 100% (159/159), 340.94 KiB | 490 KiB/s, done.
Resolving deltas: 100% (30/30), done.

C:\Users\scios>sbcl
This is SBCL 1.3.3, an implementation of ANSI Common Lisp.
More information about SBCL is available at http://www.sbcl.org/.

SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses. See the CREDITS and COPYING files in the
distribution for more information.

WARNING: the Windows port is fragile, particularly for multithreaded
code. Unfortunately, the development team currently lacks the time
and resources this platform demands.

• (ql:quickload :snark)
  To load "snark":
  Load 1 ASDF system:
  snark
  ; Loading "snark"
  [package snark-lisp]..............................
  [package snark-deque].............................
  [package snark-sparse-array]......................
  [package snark-numbering].........................
  [package snark-agenda]............................
  [package snark-infix-reader]......................
  [package snark-feature]...........................
  [package snark-dpll]..............................
  ..................................................
  ..................................................
  ..................................................
  [package snark]...................................
  [package snark-user]..............................
  ..................................................
  ..................................................
  ..................................................
  ..................................................
  ..................................................
  ..................................................
  ..................................................
  .........................
  (:SNARK)
  *

Am 01.03.2016 um 15:56 schrieb Zach Beane:

I'm using SBCL 1.3.2+.

---

Reply to this email directly or view it on GitHub:
#1084 (comment)

[quicklisp]

Quicklisp suppressed the fatal warning, sorry. You have to try with (ql:quickload "snark" :verbose t) to get it to fail.

[nilqed]

Excuse my ignorance ... I ought to know that.
I've just pushed a fix and I hope it will work now.
Thank you
Kurt

BTW: I guess SBCL is right, the "when" form was somehow incorrect.

Am 01.03.2016 um 22:00 schrieb Zach Beane:

Quicklisp suppressed the fatal warning, sorry. You have to try with (ql:quickload "snark" :verbose t) to get it to fail.

---

Reply to this email directly or view it on GitHub:
#1084 (comment)