the-little-prover / j-bob Goto Github PK
View Code? Open in Web Editor NEWLicense: BSD 2-Clause "Simplified" License
License: BSD 2-Clause "Simplified" License
With guile, I get
% guile
GNU Guile 2.0.11
Copyright (C) 1995-2014 Free Software Foundation, Inc.
Guile comes with ABSOLUTELY NO WARRANTY; for details type `,show w'.
This program is free software, and you are welcome to redistribute it
under certain conditions; type `,show c' for details.
Enter `,help' for help.
scheme@(guile-user)> (load "j-bob-lang.scm")
scheme@(guile-user)> (load "j-bob.scm")
scheme@(guile-user)> (load "little-prover.scm")
scheme@(guile-user)> (chapter1.example1)
$1 = (car (cons (quote ham) (quote (eggs))))
I thought the result was supposed to be 'ham
.
Hello! I've started reading The Little Prover and I installed ACL2 for the first time. I get errors about books not being "certified" when I try to follow the instructions in the README though. I am wondering if the error is something that I need to troubleshoot on my side or if it's a bug in this repo?
Here's the transcript running ACL2 on NixOS Linux and the latest version from this repo:
luke@thinky:~/git/j-bob/acl2]$ acl2
This is SBCL 2.0.8.nixos, 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.
ACL2 Version 8.3 built February 12, 2021 13:57:32.
Copyright (C) 2020, Regents of the University of Texas
ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
are welcome to redistribute it under certain conditions. For details,
see the LICENSE file distributed with ACL2.
Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
See the documentation topic note-8-3 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
ACL2 Version 8.3. Level 1. Cbd "/home/luke/git/j-bob/acl2/".
System books directory
"/nix/store/nhq9v7x3a2d01cx0fbcmjna04fp8xhjg-acl2-8.3/share/acl2/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(include-book "j-bob-lang")
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "j-bob-lang" ...):
Unable to load compiled file for book
/home/luke/git/j-bob/acl2/j-bob-lang.lisp
because that book is not certified. See :DOC include-book. No load
was in progress for any parent book.
ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "j-bob-lang" ...): There
is no certificate on file for "/home/luke/git/j-bob/acl2/j-bob-lang.lisp".
Summary
Form: ( INCLUDE-BOOK "j-bob-lang" ...)
Rules: NIL
Warnings: Uncertified and Compiled file
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
"/home/luke/git/j-bob/acl2/j-bob-lang.lisp"
ACL2 !>(include-book "j-bob")
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "j-bob" ...): Unable
to load compiled file for book
/home/luke/git/j-bob/acl2/j-bob.lisp
because that book is not certified. See :DOC include-book. No load
was in progress for any parent book.
ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "j-bob" ...): There is
no certificate on file for "/home/luke/git/j-bob/acl2/j-bob.lisp".
ACL2 Error in ( DEFUN REWRITE/DEFINE+ ...): It is illegal to supply
a measure for a non-recursive function, as has been done for REWRITE/DEFINE+.
To avoid this error, see :DOC set-bogus-measure-ok.
ACL2 Warning in ( INCLUDE-BOOK "j-bob" ...): The error reported above
indicates that this book is incompatible with the current logical world.
The attempted INCLUDE-BOOK has failed.
Summary
Form: ( INCLUDE-BOOK "j-bob" ...)
Rules: NIL
Warnings: Uncertified and Compiled file
Time: 0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)
ACL2 Error in ( INCLUDE-BOOK "j-bob" ...): See :DOC failure.
******** FAILED ********
is it for to make the implementation simple [about error handling] ?
or it is essential to the implementation of j-bob ?
hi Carl
it is about the scheme version of j-bob
in j-bob.scm
I see you are using (load "j-bob-lang.scm")
and
in little-prover.scm
you are using (load "j-bob.scm")
and in README.md
you said
;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")
;; Run every proof in the book, up to and including the proof of align/align:
(dethm.align/align)
note that
function redefinition is side effect
thus
this will redefine a lots of primitive functions multiple times
and use these multiple redefined functions to redefine other functions
this hurts performance
as a result
when I follow the instructions in README.md
my scheme interpreter will eat up all the memory of my machine [about 2G of memory]
you can fix this in many ways
my advice is to keep the README.md as it is
and do not use (load) in source code
When i install dracula package by raco, it tells me that it needs to install dependency planet-schematics-random1
, then it log cannot open module file \n module path: test-engine/scheme-gui
, like this:
open-input-file: cannot open module file
module path: test-engine/scheme-gui
path: C:\Program Files\Racket\share\pkgs\htdp-lib\test-engine\scheme-gui.rkt
system error: no such file or directory; rkt_err=3
compilation context...:
C:\Users\31090\AppData\Roaming\Racket\8.8\pkgs\dracula\private\scheme\test\test-drscheme.rkt
context...:
C:\Program Files\Racket\collects\racket\require-transform.rkt:266:2: expand-import
C:\Program Files\Racket\collects\racket\private\reqprov.rkt:498:5
...
There are a lot of error messages like the following at the end of the output
raco setup: error: during making for <pkgs>/dracula/drscheme
raco setup: open-input-file: cannot open module file
raco setup: module path: test-engine/scheme-gui
raco setup: path: C:\Program Files\Racket\share\pkgs\htdp-lib\test-engine\scheme-gui.rkt
raco setup: system error: no such file or directory; rkt_err=3
raco setup: compiling: <pkgs>/dracula/private/scheme/drscheme.rkt
I tried to find the reason of the error, dracula
shows on racket package webpage that the dependency it needs to install , called planet-schematics-random1.plt
doesn't exist.
I geuss that's why the installation failed.
I was wondering if there's a way to use DrRacket + Dracula integration to use J-Bob as an interactive assistant. There's seems to be a panel to the right that indicates it could show me the state of the proof Ă -lĂ Coq.
My typical mistakes are in the number of arguments or substituting a 't for a '? or that some variable isn't in scope (something a basic type-checker would point out ;-) ) which takes a while to find and all I have to troubleshoot is whether the theorem was accepted or not.
I was going through the Recess section on J-Bob, starting on page 164, when I noticed that some of the Scheme examples in little-prover.scm give incorrect results when run in MITScheme/DrRacket, but their ACL2 equivalents in little-prover.lisp give correct results when run in ACL2/DrRacket. I ran the first five Chapter 1 examples in both MIT/GNU Scheme and Dr Racket using R5RS (as described in the README) - the REPL dialogue in both interpreters proceeded as follows:
$ (load "j-bob/scheme/j-bob-lang.scm")
$ (load "j-bob/scheme/j-bob.scm")
$ (load "j-bob/scheme/little-prover.scm")
$ (chapter1.example1) ;;
-> (car (cons 'ham '(eggs))) ;; INCORRECT; should be 'ham
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> (atom (cons 'ham '(eggs))) ;; INCORRECT; should be 'nil
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> (equal 'flapjack (atom (cons a b))) ;; INCORRECT; should be 'nil
I noticed that the correct and incorrect examples differ in one key respect: the correct examples have no path to the focus (i.e., the focus is the entire expression) in their definitions, whereas the incorrect examples have at least one step with a path to the focus. Here's the same Chapter 1 examples, run with the ACL2 Dracula package in Dr Racket, showing correct output for all examples:
$ (include-book "j-bob-lang" :dir :teachpacks)
$ (include-book "j-bob" :dir :teachpacks)
$ (include-book "little-prover" :dir :teachpacks)
$ (chapter1.example1)
-> 'ham ;; CORRECT
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> 'nil ;; CORRECT
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> 'nil ;; CORRECT
Diagnosing why this is occurring is beyond my abilities at this point - can one of the authors, or someone who is more well-versed in Scheme/LISP than I am, explain what's going on here?
It took me a while to get up and running with J-Bob using the Dracula package. In particular:
When trying to use the "include-book" command in the Dr. Racket REPL, I'd get an error:
> (include-book "j-bob-lang" :dir :teachpacks)
Library/Racket/6.10.1/pkgs/dracula/lang/do-check.rkt:92:34: rename-below: defined outside of begin-below in: here
Eventually, I figured out how to do it, and I even wrote up a blog post. I recommend adding more detail to the README to make it easier on new users. I'm happy to submit a PR updating the README with the additional details.
Under the R5RS language in DrRacket, I get the error:
define-values: assignment disallowed;
cannot change constant
constant: car
which presumably means that car can't be redefined.
What version of Scheme has this been tested on? Any tips to getting it to work in DrRacket?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
đ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. đđđ
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google â¤ď¸ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.