Stream: Beginner Questions

Topic: How to count lines of code for Isabelle theories

waynee95 (Dec 22 2022 at 17:48):

Is there a tool that can count lines of code for Isabelle theory files? A tool that I use for LOC is cloc which unfortunately does not support .thy files.

It would be kinda nice if such tool could also count the number of function definitions and lemmas etc.

Manuel Eberl (Jan 04 2023 at 13:24):

I use the following language definition for cloc to count Isabelle lines, but this is a very crude approximation and there are probably lots of cases where it doesn't work properly.

Isabelle/ML
    filter remove_between_general (* *)
    extension ML
    3rd_gen_scale 3.00
Isabelle
    filter remove_between_general (* *)
    extension thy
    3rd_gen_scale 3.00

Manuel Eberl (Jan 04 2023 at 13:24):

In particular, things like text blocks are counted as code.

waynee95 (Jan 04 2023 at 16:28):

@Manuel Eberl It's a bit unfortunate that it counts text but better than nothing. Thanks!

Manuel Eberl (Jan 04 2023 at 17:06):

I'm not sure how the line counting in the AFP statistics works.

Manuel Eberl (Jan 04 2023 at 17:09):

I think proper line counting would be harder than for most languages, but still relatively feasible. One would have to be able to recognise things like normal comments, margin comments, inner syntax comments, commands like text/section/etc. and perhaps ML blocks (because those need a different parser).

Last updated: Apr 20 2024 at 08:16 UTC