Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Counting lines of code/definition vs proof?


view this post on Zulip 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

view this post on Zulip 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: Dec 05 2021 at 23:19 UTC