Bug #600
closedBLAST compatibility with Ocaml 3.11
0%
Description
It should be possible to compile BLAST with Ocaml 3.11. Currently there are some problems:
Compiling fe/ast.ml to bytecode
File "fe/ast.ml", line 213, characters 26-314:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
""
File "fe/ast.ml", line 283, characters 27-426:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
""
File "fe/ast.ml", line 1, characters 0-1:
Error: The files /usr/lib/ocaml/format.cmi
and /home/tester/ldv/ldv-tools/dscv/rcv/backends/blast/blast/include/utils/message.cmi
make inconsistent assumptions over interface Buffer
Updated by Pavel Shved over 13 years ago
- Status changed from New to Feedback
- Assignee set to Pavel Shved
That's quite funny that this bug appears in a bug tracker of verification tool suite. :-)
One of the issues with acceptance of verification tools in corporate production environments is their error reports. Better verification means more error reports. More error reports, in the minds of managers, means worse quality of the software being verified. And there's the paradox: buying better verification tools makes the quality of software worse.
Who's to blame? Of course, the managers blame those nasty verification tools! They're the root of all evil!
What does the error message says? The binary format of a compiled OCaml interface (.cmi, c stands for "compiled" in OCaml file extensions) allowed the compiler to detect binary incompatibility between use of a standard interface and its definition. It is cool! If it was C or C++, your program would just segfault upon execution, but here it's shown as an error, and you have a chance to address it!
But no, it's the verification to blame. Who reports an error contains an error. A nice way of thinking... for a corporate manager ;-).
Back to the original question, did you try to make clean first?
Updated by Pavel Shved over 13 years ago
- Status changed from Feedback to Open
Anyway, the bigger issue is to be addressed as well. The recent version of OCaml is 3.12, which was released this summer. We didn't test if BLAST compiles with it (or we did, but never wrote about it).
We should make sure that BLAST is compatible with modern compilers, and fix the problems that may arise. We have a big list of prerequisites, and it makes problems with their versions cost us much.
Updated by Alexey Khoroshilov over 13 years ago
The problem mentioned was a consequence of incomplete 'make clean' of BLAST.
After removing blast folder and checking out it again, ocaml 3.11 compiled BLAST successfully.
Updated by Pavel Shved over 13 years ago
- Category set to BLAST
Yesterday I compiled LDV tools from scratch on my machine at home (which has OCaml 3.11.2 installed), and experienced no compilation problems related to OCaml version.
But yeah, make clean should be fixed (in the utils makefile)
Updated by Pavel Shved over 13 years ago
- Status changed from Open to Closed
Well, there's been no problems with 3.11 compatibility reported, aside of absence of make clean.
I should note that make clean is buggy in BLAST, and you might need to wipe out the whole submodule and re-instantiate it.
With this note, closing.
Updated by Pavel Shved over 12 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)