Sbt test fails due to Bad Parent Session

[ianhhlee]

Complex_Bounded_Operators which is a WARN during sbt compilation but fails during test

[dominique-unruh]

I think this is because your local Isabelle distribution has no AFP configured. Configuring afp-roof in qrhl-tool.conf should help.

[ianhhlee]

There was an error in the documentation which indicated that the afp should be configured as afp-home. Changing that to afp-root allows the build to proceed.

[dominique-unruh]

I assume you mean on https://dominique-unruh.github.io/qrhl-tool/install.html? Unless there is another place where it's wrong, it's fixed now.

[ianhhlee]

Yes. That's right. Good that it was cleared up.