Hi Rob,
I discovered an issue with the latest release of ProofPower (2.8.1a17).
The system I use is Ubuntu 8.04 (Hardy Hedron). The problem has to do
with executing pp in batch mode. I do so to compile a hierarchy of
theories whose sources are distributed across multiple files; a makefile
achieves the compilation of the overall database.
I sometimes find that when executing pp in batch mode, i.e.
pp -d mydb.polyml -f myfile.doc
I get an error message that shows in the message
Aborted
after all output for the theory compilation has been display. This
happens in about %50 of the cases. In either case the database seems to
be correctly compiled and saved. The SML command that appears to be
responsible for the error is save_and_exit. I could reproduce it with
just a single instruction "save_and_exit 0;" in a file. To temporarily
fix the problem, I replace the call to "save_and_exit 0;" in pp by
(save(); ExtendedIO.system; \"sleep 0\"; exit 0)
It causes a short delay between the call to saving and exiting call.
This seems in 97% of cases to prevent the crash. The problem is
sporadic, and I think it might be caused by some sort of race conditions
i.e. a process being forcefully quit that hasn't been properly
initialised, but it is just a guess. The files imp038.doc and imp108.doc
seem to contain the code that provokes the crash. The previous versions
2.7.6 and 2.7.7 of ProofPower which I used in conjunction with Poly/ML
4.2.0 did not show the above issue. For the current version I use the
latest release 5.2 of Poly/ML. If you require more information please
let me know.
Best wishes,
Frank
--
Dr Dipl.-Inform. Frank Zeyda
Research Associate
High Integrity Systems Engineering Group
Department of Computer Science
University of York (UK)
Email: [email protected]
Phone: 0044-(0)1904-433244
WWW: http://www-users.cs.york.ac.uk/~zeyda/
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
