Disable zip feature in Bytecode mode #1248
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.
| @@ -1,2 +1,2 @@ | |||
|
|
|||
| unknown | |||
| unsat | |||
There was a problem hiding this comment.
This change is normal. I changed the test in order to use the same one for both native and SMT language.
Halbaroth
force-pushed
the
remove-my-zip
branch
from
64af396
to
1d470b9
Compare
As Basile noticed, the Javascript code in `My_zip` is dead too. I removed it and clean a bit the module. I also produces an appropriate `run error` if we try to use the feature in Javascript because `camlzip` does not work properly in bytecode. Currently, the error cannot be trigger because we do not use yet the Dolmen version of `Solving_loop` in the javascript worker. This will change in my next PR.
There was a problem hiding this comment.
The reason for the difference between the unzip.ae.zip and unzip.smt2.zip is this:
$ file tests/misc/unzip.ae.zip
tests/misc/unzip.ae.zip: Zip archive data, at least v1.0 to extract, compression method=store
$ file tests/misc/unzip.smt2.zip
tests/misc/unzip.smt2.zip: Zip archive data, at least v2.0 to extract, compression method=deflateThe unzip.ae.zip file is not compressed (method=store) while the unzip.smt2.zip file is compressed with zlib (method=deflate). Since zlib is not available with js_of_ocaml, only uncompressed zip files are supported in js_of_ocaml.
I am fine keeping the check (with the proper test, see inline comment) but I think we should remove the check for js_of_ocaml when reading zip files entirely -- if the zip file is uncompressed, it will just work; if it is compressed, we will fail due to a missing primitive anyway (it's not the nicest way to fail, but we don't expect people to actually use the jsoo version as a binary -- only through the worker).
| if Stdlib.(Sys.backend_type = Bytecode) then | ||
| Errors.unsupported_feature "Zip format in javascript mode"; |
There was a problem hiding this comment.
I believe this is disabling zip files for non-jsoo bytecode but not jsoo (which I think has Other "js_of_ocaml" as a backend type). Although I think this test should be removed entirely -- see toplevel comment.
As Basile noticed, the Javascript code in
My_zipis dead too. Iremoved it and clean a bit the module.
I also produces an appropriate
run errorif we try to use the featurein Javascript because
camlzipdoes not work properly in bytecode.Currently, the error cannot be trigger because we do not use yet the
Dolmen version of
Solving_loopin the javascript worker. This willchange in my next PR.