-
Notifications
You must be signed in to change notification settings - Fork 92
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
migrate Prover functionality from core repo #4
Conversation
had to modify some paths / folder structure / etc
…leware into add-certora-rules
@ChaoticWalrus is this good to move out of draft status? |
I marked it as a draft since it wasn't compiling / I didn't want to add to the list of these things to sort out. I'll take 15min and see if I can get it to run now after pulling from master. |
…leware into add-certora-rules
hmm, @stevennevins I'm happy to have you take a look but am still struggling here. |
Looks like a remapping issue. Adding a remappings.txt or a remappings list in the foundry.toml might resolve |
certora/applyHarness.patch
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
should this be empty?
RULE="--rule $2" | ||
fi | ||
|
||
solc-select use 0.8.12 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I noticed in the action trace you shared this command wasn't found
It's probably not remapping-related now that I took more of a look. There might be some setup piece that isn't correct or path in the config that isn't correct with the slightly different directory structure |
…leware into add-certora-rules
…ehavior from YAML file
Yeah, my bad, scripts need to also list the remappings and I missed one for 'eigenlayer-contracts'. CI should be running now but it's possible the rule still fails -- we'll see! |
we were using the wrong syntax, resulting in listing scripts twice instead of once
So this is now running as well as it was in the other repo. |
closing this PR as stale; if these rules are added, it should be in a new PR |
had to modify some paths / folder structure / etc
Marking this PR as a draft for the moment, as it's currently having compiler issues due to duplicate instances of
IPauserRegistry.sol
.