Skip to content
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

chore: tweak rpc cryptol expr parser #1215

Merged
merged 2 commits into from
Jun 11, 2021
Merged

Conversation

pnwamk
Copy link
Contributor

@pnwamk pnwamk commented Jun 9, 2021

In attempting to get saw-remote-api fully up and running
with the recent newtype changes (#1200)
I realized a slight reduction in the complexity of the previous changes
still allowed newtypes and the like to work and meant saw-remote-api
didn't have to change at all.

More specifically, the previous PR which changed the server to work with Expr Names
instead of Expr PNames was not actually necessary. This commit removes those
specific changes and brings things back to the parser-level world of syntax (Expr PName).

@pnwamk
Copy link
Contributor Author

pnwamk commented Jun 10, 2021

Regarding the CI failures, I think they are unrelated...

  • build-push-image (Dockerfile, ghcr.io/galoisinc/cryptol, ghcr.io/galoisinc/cache-cryptol)
Run docker/build-push-action@v2                  2h 47m 30s

I'm not sure why it's handing on that step. I don't understand how these changes could impact that.

  • build-push-image (PORTABILITY=true, cryptol-remote-api/Dockerfile, ghcr.io/galoisinc/cryptol-remo...
Image: "test-cryptol-remote-api:latest" with ID "sha256:f4c53fdce5335bc68a7e9e7843988c5a84cda9ddef7e530ab32eb1aa7f9cfb02" not yet present on node "kind-control-plane", loading...
ERROR: failed to load image: command "docker exec --privileged -i kind-control-plane ctr --namespace=k8s.io images import -" failed with error: exit status 1

Command Output: unpacking docker.io/library/test-cryptol-remote-api:latest (sha256:5bf6036ac4101146fdcb7ffce49d8a21de4e7052b295d774c7765f53bf7f7bc8)...time="2021-06-10T18:25:07Z" level=info msg="apply failure, attempting cleanup" error="failed to extract layer sha256:dd3097cd7909834b61bdd207dcf8dd6e4db35b638f643c6ccfd5ef1a58c3b7ae: write /var/lib/containerd/io.containerd.snapshotter.v1.overlayfs/snapshots/71/fs/usr/lib/x86_64-linux-gnu/librsvg-2.so.2.44.10: no space left on device: unknown" key="extract-367102904-QyYu sha256:8245467a6af5775eb6375049e95546f5795a2bd9f167cd29e1abc8c860ef777f"
time="2021-06-10T18:25:07Z" level=warning msg="extraction snapshot removal failed" error="write /var/lib/containerd/io.containerd.metadata.v1.bolt/meta.db: no space left on device: unknown" key="extract-367102904-QyYu sha256:8245467a6af5775eb6375049e95546f5795a2bd9f167cd29e1abc8c860ef777f"
ctr: failed to extract layer sha256:dd3097cd7909834b61bdd207dcf8dd6e4db35b638f643c6ccfd5ef1a58c3b7ae: write /var/lib/containerd/io.containerd.snapshotter.v1.overlayfs/snapshots/71/fs/usr/lib/x86_64-linux-gnu/librsvg-2.so.2.44.10: no space left on device: unknown

Seems highly unlikely to be related to these changes.

  • test (test-lib, regression, ubuntu-latest, false)
> What4 exception:
> Could not parse solver response:
>   SApp [SAtom "error",SString "Parse Error: Illegal argument detected\n\n  (set-logic ALL_SUPPORTED)\n             ^\n\nvoid cvc5::LogicInfo::setLogicString(std::__cxx11::string)\n\n  `logicString' is a bad argument\nLogicInfo::setLogicString(): junk (",SAtom "LL_SUPPORTED",SString ") at end of logic string: ALL_SUPPORTED"]
> in response to commands:
>   (check-sat)

is a failure in cryptol's regression tests and not related to the server or any changes made.

  • test (rpc, windows, true)
Started 2h 34m 42s ago

Starting workflow run...

I'm not sure if this job is just waiting for resources or what, but it appears to not be starting and/or making initial progress.

Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM from a cursory glance. We should open dedicated issues about the CI failures in case they arise again.

@pnwamk pnwamk merged commit 36475d1 into master Jun 11, 2021
@pnwamk pnwamk deleted the rpc/modify-expression-parser branch June 11, 2021 15:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants