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


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,

 Dr Dipl.-Inform. Frank Zeyda
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Email: ze...@cs.york.ac.uk
 Phone: 0044-(0)1904-433244
 WWW: http://www-users.cs.york.ac.uk/~zeyda/

Proofpower mailing list

Reply via email to