On 27 Jun 2014, at 17:53, David Matthews <[email protected]> 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.
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
