Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error of installing isabelle-linter in Isabell...

view this post on Zulip Email Gateway (Oct 30 2022 at 07:30):

From: 伊藤洋介 <glacier345@gmail.com>
Dear isabelle-linter developers,

Today I successfully installed Isabelle2022, but I could not install
isabelle-linter in the same way as Isabelle2021-1.
I use MacBook Air (M1, 2020), macOS Monterey, ver.12.6.

I downloaded "isabelle-linter-Isabelle2021-1-v1.0.0" from
https://github.com/isabelle-prover/isabelle-linter
and moved the directory to
/Applications/Isabelle2022.app/contrib
After adding "contrib/isabelle-linter-Isabelle2021-1-v1.0.0" to
/Applications/Isabelle2022.app/etc/components
I started Isabelle/jEdit, but I got the following error.

type Zoom_Box is not a member of object isabelle.jedit.Font_Info
value factor is not a member of Object
Found: (Linter_Dockable.this.zoom : Object)
Required: scala.swing.AbstractButton
3 errors found
-- [E008] Not Found Error:
/Applications/Isabelle2022.app/contrib/isabelle-linter-Isabelle2021-1-v1.0.0/jedit_linter/src/linter_dockable.scala:195:35

195 | private val zoom = new Font_Info.Zoom_Box { def changed =
handle_resize() }
| ^^^^^^^^^^^^^^^^^^
| type Zoom_Box is not a member of object isabelle.jedit.Font_Info
-- [E008] Not Found Error:
/Applications/Isabelle2022.app/contrib/isabelle-linter-Isabelle2021-1-v1.0.0/jedit_linter/src/linter_dockable.scala:71:66

71 | Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
| ^^^^^^^^^^^
| value factor is not a member of Object
-- [E007] Type Mismatch Error:
/Applications/Isabelle2022.app/contrib/isabelle-linter-Isabelle2021-1-v1.0.0/jedit_linter/src/linter_dockable.scala:198:111

198 | Wrap_Panel(List(linter_button, auto_lint_button, lint_all_button,
show_descriptions_checkbox, lint_button, zoom))
|
^^^^
| Found: (Linter_Dockable.this.zoom : Object)
| Required: scala.swing.AbstractButton
|
| longer explanation available when compiling with -explain
3 errors found
*** Failed to compile Scala sources

Am I wrong with installing, or is isabelle-linter not yet maintained for
Isabelle2022?
Any advice is appreciated.

Best regards,

view this post on Zulip Email Gateway (Oct 30 2022 at 08:08):

From: Jan van Brügge <jan@vanbruegge.de>
Hi,
if you download the current master, the linter works.
Cheers
Jan

Oct 30, 2022 7:30:01 AM 伊藤洋介 <glacier345@gmail.com>:

view this post on Zulip Email Gateway (Oct 30 2022 at 09:30):

From: 伊藤洋介 <glacier345@gmail.com>
Dear Jan van Brügge,

Thank you for the reply.
It did work well!
This plugin is very helpful.
I really appreciate your help.

Best regards,

2022年10月30日(日) 17:07 Jan van Brügge <jan@vanbruegge.de>:

Last updated: Apr 25 2024 at 04:18 UTC