Re: [isabelle] 2014-RC1 issues

On Fri, 1 Aug 2014, Lars Noschinski wrote:

An issue with symlinks:

Given file a file "/home/lars/projekte/test.ML" and symlink
"/home/lars/P" to "projekte" and a theory

theory Scratch imports Pure

ML_file "/home/lars/P/test.ML"


Then a click on the file name will open the correct file, but without any annotations.

The prover will open the wrong file, i.e. the one that is stored on the file-system, instead of taking the buffer content from the editor as expected. After some editing of the buffer, the divergence will become apparant. The lack of detailed markup is a consequence of not going through PIDE.

The superficial reason for that is a small mistake how PIDE document node names are produced, with a disagreement about canonical forms due to symblinks. This will work in the next release candidate.

The deeper problem is a confusion about responsibilities: the prover still accesses the file-system as a fall-back, when the Prover IDE did not do that. Thus mistakes in providing file content are silently turned into unintended behaviour.

As explained earlier, this mixed responsibility is there to allow Isabelle/HOL itself to be edited interactively on a small mobile device of only 4--8 GB.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.