Email Gateway (Nov 14 2020 at 04:11): Email Gateway (Nov 14 2020 at 04:11):From: Jason Gross <jasongross9@gmail.com>
Hi,
Is there a tool that can tell me how many lines in a .thy file are
whitespace/comments vs definitions vs proofs? (I'm looking for something
analogous to coqwc.)
Thanks,
Jason
Email Gateway (Nov 19 2020 at 13:55):From: Makarius <makarius@sketis.net>
I would say that classic existence holds: people surely have their own tools
for particular projects, without making it explicit.
The general approach is to use Isabelle/Scala for such "systems programming"
around Isabelle. This gives proper access to the structure of sessions,
theories, commands within theories etc. including the all-important "outer
syntax".
(Note that Isabelle syntax can be augmented locally, e.g. Isabelle/ZF has
slightly different commands s different Isabelle/HOL, or applications can add
their own commands on the spot.)
To demonstrate this in practice, I've put together such a tool on the spot, as
external Isabelle/Scala script wc.scala in the sense of the Isabelle "system"
manual, section 1.2.
To activate that, you can put it e.g. into $ISABELLE_HOME_USER/Tools/wc.scala
and register the enclosing directory in $ISABELLE_HOME_USER/etc/settings like
this:
ISABELLE_TOOLS="$ISABELLE_TOOLS:$ISABELLE_HOME_USER/Tools"
(The location of $ISABELLE_HOME_USER is platform-specific, but you can open
that symbolic name literally in Isabelle/jEdit directory browser, or you use
"Isabelle2020/bin/isabelle getenv ISABELLE_HOME_USER" on the command line.)
Here are some example invocations:
Isabelle2020/bin/isabelle wc -D '~~/src/FOL'
Isabelle2020/bin/isabelle wc -a
Isabelle2020/bin/isabelle wc -d afp-2020/thys -a
(The latter requires a clone/download of
https://foss.heptapod.net/isa-afp/afp-2020 )
If you want to understand Isabelle/Scala concepts and modules, you can use
"isabelle scala_project" together with IntelliJ IDEA and Gradle, as explained
in the "system" manual, section 5.5.
If you want to make a statically compiled Isabelle/Scala addon-tool, it is
better to wait a few weeks until the release process for Isabelle2021 starts:
that will provide official interfaces to add Scala jar modules in user space.
The actual counting of things within a theory node is a different question:
the structure is quite complex, this is not "program code" with comments as in
the 1970ies. There are first-class document commands like 'text', 'section',
'chapter', as well as embedded formal and informal comments. In my example
implementation, I've merely explored "command spans" in the sense of good-old
(and retired) Proof General.
An alternative is to look e.g. into
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Isar/document_structure.scala
Or you can be more ambitious and inspect theory content after formal
processing by the Isabelle/ML prover process. The "isabelle dump" tool is an
example for that, without doing anything in particular, see
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Tools/dump.scala
Makarius
wc.scala
Last updated: Jul 15 2022 at 23:21 UTC