Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Execute model checkers in a temporary directory #33

Closed
andrey-kuprianov opened this issue Mar 22, 2021 · 1 comment · Fixed by #48
Closed

Execute model checkers in a temporary directory #33

andrey-kuprianov opened this issue Mar 22, 2021 · 1 comment · Fixed by #48
Assignees
@andrey-kuprianov

Comments

@andrey-kuprianov
Copy link
Contributor

Currently the model checkers (Apalache and TLC) are run in the same directory where the executable is called. This pollutes the directory, and also has the possibility of name clashes. We need to execute model checkers in a temporary directory, similar to how it's done in Tendermint-rs LightClient tests. This also simplifies the cleanup task -- simply delete the tempdir.
@andrey-kuprianov andrey-kuprianov mentioned this issue Apr 12, 2021
Closed
@andrey-kuprianov andrey-kuprianov self-assigned this May 12, 2021
@andrey-kuprianov
Copy link
Contributor Author

This is necessary in order to fix #43, which in turn is a prerequisite for #44.

andrey-kuprianov added a commit that referenced this issue Jul 16, 2021
@andrey-kuprianov
towards #33: copy TLA files into a tempdir
72cd2b9
This was referenced Jul 19, 2021
Closed
Closed
andrey-kuprianov added a commit that referenced this issue Jul 19, 2021
@andrey-kuprianov
close #33: use tempdir as curdir; disble incompatible tests
c635231
@andrey-kuprianov andrey-kuprianov mentioned this issue Jul 19, 2021
Merged
andrey-kuprianov added a commit that referenced this issue Jul 21, 2021
@andrey-kuprianov @rnbguy
Execute model checkers in a temporary directory (#48)
b5148c6 
closes #33 : 
* copy TLA files into a tempdir
* use tempdir as curdir; disble incompatible tests
* allow unused_imports, dead_code at crate level
* remove walkdir dependency


Co-authored-by: Ranadeep Biswas <ranadeep@informal.systems>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andrey-kuprianov andrey-kuprianov

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Execute model checkers in a temporary directory informalsystems/modelator
1 participant
@andrey-kuprianov