-
Notifications
You must be signed in to change notification settings - Fork 33
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
Remove My_zip module #1264
Remove My_zip module #1264
Conversation
We should use the same test as we only want to check that Alt-Ergo can unzip correctly the input file if its name has the form: name.format.zip.
The module `My_Zip` contains only function which is called once in `Solving_loop`. This commit cleans the code and move it in `Solving_loop` directly. Technically, `Solving_loop` is a part of the binary, but as everyone knows, most of the code of this module will be push into the library after we design a good API.
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 good to me. What are the changes to unzip.ae.zip
and unzip.smt2.zip
and why are they needed?
They did not contain the same test (up to translation). We only want to check that Alt-Ergo can unzip archives and recognize the right format based on the name of the archive. It would be annoying that one of them fails because the zipped test fails. |
Ah yes this is the issue that one is zipped with compression and not the other. We should keep one test for compressed zip and one test for uncompressed zip however. Can we instead rename them to be explicit (e.g. |
Now, there are both uncompressed:
and
I guess that If you want, I can force the method with the option |
Please do keep a test with a compressed zip file. It is a use case we want to support so it should be in the test suite. |
Done. The option |
Add a padding comment in both tests to ensure that zip won't choose the store method while compressing them.
The module
My_Zip
contains only function which is called once inSolving_loop
. This commit cleans the code and move it inSolving_loop
directly. Technically,Solving_loop
is a part of thebinary, but as everyone knows, most of the code of this module will be
push into the library after we design a good API.
This PR replaces #1248