[isabelle-dev] Final consolidation for Isabelle2018-RC2

Makarius makarius at sketis.net
Fri Jul 20 03:18:42 CEST 2018


On 19/07/18 13:42, Tobias Nipkow wrote:
> I have the same problem, and on my machine it is reproduceable (and it
> did not go away over the past week, although I tried different versions
> of the devel repository).

I suspect that it is a deferred error due to lazy facts in locale
interpretation.

In Isabelle/5820f0f379ae, I have now added the system option
"strict_facts" to avoid this.

You can use it with "isabelle build -o strict_facts" or add it
temporarily to $ISABELLE_HOME_USER/etc/preferences as "strict_facts =
true" (notably for "isabelle jedit").


	Makarius




More information about the isabelle-dev mailing list