Skip to content

Update simple-untyped to work with the modern backends.#2841

Merged
rv-jenkins merged 21 commits intodevelopfrom
simple-untyped-llvm
Nov 10, 2022
Merged

Update simple-untyped to work with the modern backends.#2841
rv-jenkins merged 21 commits intodevelopfrom
simple-untyped-llvm

Conversation

@nishantjr
Copy link
Copy Markdown
Contributor

@nishantjr nishantjr commented Aug 30, 2022

All tests pass with the k-exercises updateSimpleUntyped branch.

@nishantjr nishantjr requested review from dwightguth and xc93 August 30, 2022 22:41
@nishantjr nishantjr force-pushed the simple-untyped-llvm branch from 52709ef to b694bed Compare August 30, 2022 22:44
@ehildenb ehildenb changed the base branch from master to develop September 27, 2022 20:44
Copy link
Copy Markdown
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

btw --bound works now

#Equals
"3 2 "
}
#Or
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I expected us to lose some behaviors in some cases, but why have we gained behaviors?

Copy link
Copy Markdown
Contributor Author

@nishantjr nishantjr Oct 18, 2022

Choose a reason for hiding this comment

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

I'm not sure why the original output had only two behaviours (maybe something to do with needing to label transitions in the Java backend?). Looking at both the semantics of the language, and the comment in the program, it seems that 4 behaviours are to be expected.

@nishantjr
Copy link
Copy Markdown
Contributor Author

btw --bound works now

OK, thanks. Looks like there are some additional ==K vs #Equals changes that I somehow missed.

@radumereuta radumereuta requested a review from a team as a code owner November 7, 2022 17:27
Comment thread .github/workflows/test-pr.yml Outdated
@radumereuta radumereuta self-assigned this Nov 8, 2022
@jberthold
Copy link
Copy Markdown
Collaborator

Looked at the macos build failure - maybe we should configure the extra nix cache for Haskell infrastructure? See the setup for the haskell-backend

signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
name: k-framework
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

@jberthold we do set up the extra_nix_config here, but it doesn't run on our own CI machines, so I guess it's not actually using taht. We could add back extraPullNames: kore, but I'd like to consolidate caches.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

What I meant to suggest was to add the https://cache.iog.io substituter (IOHK Haskell infra cache), in "Install Nix".
We do this about 8 lines above here but the test-nix job in https://github.com/runtimeverification/k/blob/91f11338d4ccf3626f4e8874e10071e09d5131c6/.github/workflows/test-pr.yml#L192..L198 does not add that cache.
Thought it would be worth a try

@rv-jenkins rv-jenkins merged commit 9f56cda into develop Nov 10, 2022
@rv-jenkins rv-jenkins deleted the simple-untyped-llvm branch November 10, 2022 10:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

6 participants