Admin/isatest-lint
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 16309 39c793a9b382
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16309
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     1
#!/usr/bin/env perl
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     2
#
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     3
# $Id$
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     4
# Author: Florian Haftmann, TUM
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     5
#
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     6
# Do consistency and quality checks on the isabelle sources
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     7
#
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     8
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
     9
use strict;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    10
use File::Find;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    11
use File::Basename;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    12
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    13
# configuration
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    14
my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    15
my @suffices = ('\.thy', '\.ml', '\.ML');
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    16
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    17
# lint main procedure
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    18
sub lint() {
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    19
    my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    20
    if ($ext) {
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    21
        open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    22
        my $found = 0;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    23
        while (<ISTREAM>) {
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    24
            $found ||= m/\$Id[^\$]*\$/;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    25
            last if $found;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    26
        }
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    27
        close ISTREAM;
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    28
        my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    29
        if (! $found) {
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    30
            print "Found no CVS id in $relname\n";
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    31
        }
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    32
    }
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    33
}
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    34
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    35
# first argument =^= isabelle repository root
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    36
if (@ARGV) {
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    37
    $isabelleRoot = $ARGV[0];
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    38
}
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    39
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    40
find(\&lint, $isabelleRoot);
39c793a9b382 added isatest-lint prototype
haftmann
parents:
diff changeset
    41