-
Notifications
You must be signed in to change notification settings - Fork 31
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
New instances syntax #739
New instances syntax #739
Conversation
@@ -283,23 +283,23 @@ quint run --init=Init --step=Next --seed=abcde --max-steps=4 \ | |||
An example execution: | |||
--------------------------------------------- | |||
action step0 = all { | |||
counters::n' = 1, | |||
n' = 1, |
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.
This works because we only need to evaluate the main module now that it is self-contained by flattening. WDYT @konnov ? Is there something I'm missing here or is this great? 😅
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.
Perhaps this ended up being a solution to #731 ?
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.
Yes, these traces look much better now! I was also annoyed by counters::
.
@@ -8,7 +8,7 @@ false | |||
true | |||
-40 | |||
104 | |||
runtime error: error: Variable kettle::temperature is not set | |||
runtime error: error: Variable temperature is not set |
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 changed this and the markdown by hand because setting up a go env to build lmt
didn't fit my schedule for this week 😝. I hope it doesn't break automatic generation.
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.
Looks great! Amazing work. I left just a few comments.
const lastId = modules.map(m => m.id).sort((a, b) => Number(a - b))[modules.length - 1] | ||
const idGenerator = newIdGenerator(lastId) |
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 am worried about this computation. This looks fragile to me. If other code is using a global id generator (which we kind of have in CLI commands), this local id generator will go ahead and produce conflicting ids. This will be very hard to debug in the future. Can we pass an id generator as a parameter?
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.
Hm, I think that if other code is using a "global" id generator, than other code is wrong 😅. Atm, we only use id generators on parsePhase1
and here. If we use it somewhere else, I think we should do some check similar to this one, to make sure that it is initialized in a valid state. Otherwise, we might as well have an actual global state as you suggested the first time, which has all the problems we already mentioned.
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.
The simulator converts runtime values back to QuintEx
. That's where it can introduces new identifiers, which would clash with the identifiers here.
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.
But the ids generated in toQuintEx
are not used for anything, right? If we did use them, we should find a way to get the original ids back somehow (by storing them in the runtime value, for example). The current ids used there won't have a source map entry nor a lookup table entry for them, so anything would most likely break if we tried to use them.
If there's no real problem in the clashing right now, I'd like to merge this and take a look at this generator problem again. I don't think simulating a global state is a good solution here.
switchModule(moduleId: bigint, moduleName: string) { | ||
this.currentModule = { id: moduleId, name: moduleName } | ||
} | ||
|
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.
This is so good that we don't have to worry about multiple modules now!
const tableA = collectDefinitions(moduleA) | ||
const lookupTableA = resolveNames(moduleA, tableA, treeFromModule(moduleA)).unwrap() | ||
|
||
const module = buildModuleWithDefs(defs, undefined, idGenerator) | ||
const module = result.value.modules[1] |
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.
not sure, why there is moduleA
and module
? Can we rename module
to moduleB
?
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.
module
is like a main module here, and moduleA
is the module called A
imported by module
. I'll add some comments.
Hello
This introduces our new syntax for instances, introduced in ADR 6, which closes #724. In order to use that syntax in a nice way, I needed to combine it with imports (see the Tendermint example), so I also implemented flattening for modules, which closes #11.
With flattened modules, the main module is now self contained and we only need to evaluate that single module in the REPL. So I have removed some support for multiple modules in the compiler, which makes variable names easier to read. But that broke error reporting since source maps for flattened modules were still not consistent. So, I also fixed the source map problem, which closes #730.
npm run format
(or had formatting run automatically on all files edited)CHANGELOG.md
for any new functionalityREADME.md
updated for any listed functionality