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.

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

Clean verif/ directory before writing to it #1303

Merged
merged 3 commits into from
Jan 27, 2025
Merged

Conversation

Lysxia
Copy link
Collaborator

@Lysxia Lysxia commented Dec 11, 2024

When you remove a function in your Rust code, the corresponding Coma file(s) should be removed.

@Lysxia Lysxia force-pushed the remove-coma-files branch 2 times, most recently from a84d25f to a0ef848 Compare December 11, 2024 18:31
@arnaudgolfouse
Copy link
Collaborator

Hm, this is not enough unfortunately: removed files are still listed in the why3session.xml, and they cause a crash in why3...
Granted, why3find handles it without issues ;) (But I need the ide and its tactics)

@Lysxia
Copy link
Collaborator Author

Lysxia commented Dec 12, 2024

I think we want to fix why3 here.

@Lysxia
Copy link
Collaborator Author

Lysxia commented Dec 23, 2024

This should resolve the crash https://gitlab.inria.fr/why3/why3/-/merge_requests/1189

@jhjourdan
Copy link
Collaborator

This should resolve the crash https://gitlab.inria.fr/why3/why3/-/merge_requests/1189

Is this really what we want? Who is going to remove the session file in this case?

@Lysxia
Copy link
Collaborator Author

Lysxia commented Jan 27, 2025

My Why3 MR addresses the current/old use case of having one big why3session.xml at the root of the project for all .coma files, by fixing the crash when a file is removed and instead treating its session as detached.

Since then, we've also decided to switch to a workflow where each .coma file has its own why3session.xml or proof.json, and this workflow does not run into the crash above. As far as I can tell, dangling why3session.xml files are harmless. Removing them as soon as we remove their .coma file seems dangerous (the user could change their mind and re-add the .coma file, or they may want to move the session/proof file rather than delete it). Instead I propose to add a new command cargo creusot clean to remove dangling sessions and proofs. cargo creusot could suggest this command in a warning.

@jhjourdan
Copy link
Collaborator

Sounds good indeed!

@jhjourdan jhjourdan enabled auto-merge January 27, 2025 10:13
@jhjourdan
Copy link
Collaborator

Ok, this looks good to me. Merging as soon as CI passes.

@jhjourdan jhjourdan merged commit 55636f6 into master Jan 27, 2025
6 checks passed
@jhjourdan jhjourdan deleted the remove-coma-files branch January 27, 2025 10:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants