search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

Remove My_zip module #1264

Closed Halbaroth closed 3 weeks ago

Halbaroth commented 3 weeks ago

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.

This PR replaces #1248

Halbaroth commented 3 weeks ago

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.

bclement-ocp commented 3 weeks ago

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. unzip_compressed.ae.zip and unzip_uncompressed.smt2.zip, or the opposite, I don't remember which is which)?

Halbaroth commented 3 weeks ago

Now, there are both uncompressed:

file unzip.ae.zip 
unzip.ae.zip: Zip archive data, at least v1.0 to extract, compression method=store

and

file unzip.smt2.zip
unzip.smt2.zip: Zip archive data, at least v1.0 to extract, compression method=store

I guess that zip chooses automatically the compression method based on the size of the file. Compressing a tiny file will produce a table larger than the file itself, so zip chooses the store method.

If you want, I can force the method with the option -Z, but I think it does not matter.

bclement-ocp commented 3 weeks ago

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.

Halbaroth commented 3 weeks ago

Done. The option -Z cannot force zip to compress file. So I added a padding comment in both tests to ensure that they will be compressed.