On 27 Jun 2014, at 17:53, David Matthews <David.Matthews at prolingua.co.uk> wrote:
On 27/06/2014 12:03, Makarius wrote:
What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there?
Poly/ML always creates a .polyml directory and a poly-stats file. The poly-stats file will be deleted when the Poly/ML process finishes normally. If it crashes, though, the file will remain.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the shared-memory file be for global stats only?
The Poly/ML process does not know when another process wants to read the statistics so they are always made available as a memory-mapped file.
I discovered the same problem with ProofPower where users run via a GUI which just kills the ProofPower executable when the user quits or asks to restart the ProofPower session. It is a bit surprising that running a stand-alone program (like Joe Hurd?s opentheory or my slrp parser generator) creates $HOME/.polyml and that aborting a run with Ctrl+C leaves a stats file in that directory.
The files are only 4096 bytes so it is not much of an overhead, but it is a bit messy. Would it make sense to provide a function in PolyML.Statistics allowing a process to opt into making its statistics available? (Or conversely, is there a requirement to access statistics from a program that has not been designed with that in mind?)
Regards,
Rob.