Interactive merger! #44
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Currently only "Open" is actually reported. This is for the interactive UI later on.
`OrVec` is used as an Either to properly serialize to JSON.
Currently shown in the hint area (status bar). This should be temporary.
It is actually in milliseconds in the config.
The `linesIterator` thingy.
When calling `smt.disableLogging`. Disable only SMT-related loggers.
Using "." for `getParentDir` rarely makes sense.
For interaction.
Just runs `Synthesis` and sends the next step as JSON.
So this is what I'm doing with my life now, huh.
A bunch of security vulnerabilities in `cssnano`. They're meaningless, but welp.
Easier to manage, and for now there is some state in the server still.
Display choices, waits for user selection.
For exploring interactively in client-server mode.
Display more info with choices: goal from which each choice was derived and name of rule. Update status when sent from server.
Also serve static HTML/JS/CSS from `SynthesisServer`.
`ProofTrace.updateIndex` is becoming quite a monster.
And derivation trail for SubstL/R.
Allows the client to send defs and pre-/post-condition. This is very much a wip, and some of the stuff in `ClientSessionSynthesis` should probably move up to `SynthesisServer`.
For serving on the web.
Serialize formula ASTs. Refactor the interaction protocol's client message format.
The protocol functionality is still there, but UI interaction is TBD.
Some benchmarks have config flags on the first line, without which they fail to synthesize.
Limit zoom to 10%-100%. Fade all messages when clearing them.
Instead of labels, which are not unique across OrNode child siblings.
For AndNodes, show only last rule label. For OrNodes, separate rule labels with ▹.
Aren't we picky.
Otherwise the goals just keep growing and get pretty hairy!
For Akka (esp. `reference.conf`).
Some syntax has been deprecated: `in` method.
Filename is still needed because scopt, but ignored. E.g. `suslik server .`
Emits log to file in `logs/`. Uses rolling log appender.
Each synthesis task is limited to one hour. Timeout can be specified as e.g. `10s` instead of `10000` for convenience.
Turns out submodules tracking a branch can be forwarded with git submodule update --remote
Conflicting build.sbt configs and a change in the command-line args format.
It's the little things.
For interactive frontend.
Less confusing.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I have merged the
interactivefunctionality withmaster. The number of changes is still kind of large, so a full code review is probably not an option, but at least maybe you can run the test suite and see whether the things that fail should fail?