-
Notifications
You must be signed in to change notification settings - Fork 96
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Nonstd build failing in projects/sat/proof-checker-array #674
Comments
I've invited nwetzler to the team, but he has to accept the invite before we can tag him. |
MattKaufmann
added a commit
that referenced
this issue
Nov 30, 2016
Thanks for fixing this, Matt. It looks like it's because I used "rationalp" where you need "real/rationalp" for ACL2r. Should I try building any future commits with ACL2r before merging? |
Hi, Nathan --
Right -- it was an easy fix (just a couple such changes). My (strong)
opinion is that it's too much of a burden to run with ACL2(r) before
checking in -- I virtually never do so, anyhow, unless it's for a
release.
…-- Matt
Date: Sun, 04 Dec 2016 12:36:36 -0800
From: Nathan Wetzler ***@***.***>
Reply-To: acl2/acl2 ***@***.***>
Cc: MattKaufmann ***@***.***>,
State change ***@***.***>
[1:text/plain Hide]
Thanks for fixing this, Matt. It looks like it's because I used "rationalp" where you need "real/rationalp" for ACL2r. Should I try building any future commits with ACL2r before merging?
--
You are receiving this because you modified the open/close state.
Reply to this email directly or view it on GitHub:
#674 (comment)
[2:text/html Show]
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Probably this should just be fixed by putting
;; cert-param: (non-acl2r)
in any books that need them, but optionally someone could try to make them compatible with acl2(r).
I can't seem to assign this to @nwetzler (anyone know why?) but anyone with a little time to build acl2(r) and the relevant books could probably fix this.
The text was updated successfully, but these errors were encountered: