search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Bring back the TLA+ extraction. #57

Closed VictorCMiraldo closed 2 years ago

VictorCMiraldo commented 2 years ago

Pull-request #56 removed TLA+ from our WIP branch; that branch is on its way to become Pirouette's main branch at some point in the coming weeks. Once our symbolic-execution engine is working and well-tested, we must bring TLA+ back. We hope that this second iteration will be much easier since a lot of the hard work will have been performed at the pirouette internal representation level (i.e., monomorphization, defunctionalization, specialization, etc...).

While we're at it, we should look into the TLA+ issues that we had open before, which have been closed since we're pivoting pirouette.

VictorCMiraldo commented 2 years ago

Changed priorities since the current focus is moving further away from TLA+ extraction.

VictorCMiraldo commented 2 years ago

There are many other priorities and more interesting analyses to implement in Pirouette; I'll close this one.