Re: [isabelle] Isabelle2019-RC2: Experience report

Hi List,

an initial experiment on porting my current ~42kLOC project from
2018 to RC2 went surprisingly well. 

I only encountered a few changes not explicitly covered by NEWS:
 * There are various renamings in HOL-Words, and maybe also simpset
changes (?). This is not explicitly mentioned by the NEWS entry.

 * The ML-Level interface of intro_locales_tac changed. The new 
  "strict" and "eager" flags are not documented at all, I figured out
the right combination for me by trial and error.

 * Finally, the option Syntax_Trans.eta_contract_raw disappeared. Its
now just eta_contract, and properly typed!

 * A few proofs involving {auto,fastforce} and combinations of split:
and split!: stopped to work, and had to be re-done more explicitly. I
have not figured out the exact reason.

 * My project involves a custom code generator. I am still using an
implementation that I adapted from the 2018 standard code generator for
generating files relative to the theory folder. This still works, but I
understand that I have to port it to the new VFS idiom.

The following (already reported) issues remain:
  * The fonts still look more blurry than in 2018, on my full HD screen
  * The NEWS file does not specify any replacement for old style inner
comments (* *). The entry for Isabelle-2018 says to use \comment or
\cancel. However, content of \comment is interpreted as latex text,
causing trouble with unknown antiquotations when e.g. trying to comment
out "{1,2}@{a,b}". Moreover, \cancel used to occur in "striked out"
style in Latex output, at least when used in outer syntax. Is this also
the case for inner-syntax \cancel? Can I make parts of inner syntax
disappear from latex output?


On Sa, 2019-05-11 at 19:30 +0200, Makarius wrote:
> Dear Isabelle users,
> we are getting one step closer to the Isabelle2019 release, which is
> ultimately scheduled for the first half of June 2019.
> The consolidated release candidate Isabelle2019-RC2 is now available
> from -- it
> corresponds to AFP version
> The blog entry
> is
> continuously updated to follow the release process.
> Everything is ready and pretty stable. We need more serious testing
> to
> produce counter-examples to this claim.
> When discussing release candidates, please provide a mail Subject
> line
> that fits to the content, not just a clone of the announcement.
> 	Makarius

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