-
Notifications
You must be signed in to change notification settings - Fork 3
/
pre-commit-coq
executable file
·337 lines (285 loc) · 9.73 KB
/
pre-commit-coq
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
#!/usr/bin/perl -w
use strict;
use warnings;
use File::Temp qw/ tempfile tempdir /;
use File::Copy;
use File::Basename;
use File::Spec;
use Cwd;
use lib '.perl';
# this is required to untaint backticks -
# not sure if we will go all the way to untainting
$ENV{"PATH"} = "/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin";
sub pc_pad {
my $str = shift;
chomp $str;
return ("[pre-commit] $str\n");
}
# I think there's a slicker way to do this, using output filters, but
# for now let's just do this as a subroutine.
sub pc_print {
my $str = shift;
chomp ($str); # in case it already had some extra whitespace at the end
print (pc_pad ($str . "\n"));
}
my $wikilock;
# maximal number of changes in one commit/push
my $MAX_CHANGED_NBR = 10000;
sub pc_die
{
pc_print(@_);
die();
}
my $cwd = getcwd ();
# untaint
if($cwd =~ /(.*)/) { $cwd = $1; }
# Compute list of itp files that belong to the index (i.e., the
# itp files that are about to be committed). git diff-index will
# give a list of changed files. We compare the index to HEAD, the
# most recent commit known to be valid/coherent. The actual file name
# is the second field of the line (where the field separator is tab),
# hence the first call to "cut -f 2". The last cut gives us
# "semiring" from "semiring.v" and "polyform" from "polyform.miz".
my $mizar_article_ext = 'miz';
my $coq_article_ext = 'v';
my $article_ext = $coq_article_ext;
my $article_regexp = '\.$article_ext\$';
# Articles changed.
# We do not check if they are inside the "lib" directory here yet.
my @art_changed
= `git diff-index --cached HEAD | cut -f 2 | grep '\.$article_ext\$'`;
my @non_art_changed
= `git diff-index --cached HEAD | cut -f 2 | grep --invert-match '\.$article_ext\$'`;
if(scalar (@non_art_changed) > 0) {
pc_print ("Only .$article_ext files are permitted to be committed: \"$non_art_changed[0]\" Sorry.");
exit (1)
}
elsif($#art_changed > $MAX_CHANGED_NBR) {
pc_print ("Only $MAX_CHANGED_NBR files are permitted to be changed in one commit/push: $#art_changed Sorry.");
exit (1)
}
# The changed articles inside the "lib" directory
my @lib_changed = ();
my @non_lib_changed = ();
# Get a value for a mwiki variable either from environment (uppercase)
# or from git config (lower case).
# The input is expected as lower case.
sub get_mwiki_var
{
my ($varname) = @_;
my $result;
if (defined ($ENV{uc($varname)}))
{
$result = $ENV{uc($varname)};
}
else
{
my $git_output = `git config mwiki.$varname`;
my $git_exit_code = ($? >> 8);
if ($git_exit_code == 0)
{
chomp($git_output);
$result = $git_output;
}
else { return undef; }
}
return $result;
}
# MAKEJOBS: number of different make jobs to run simultaneously
my $makejobs = 1;
my $tmp1 = get_mwiki_var("makejobs");
$makejobs = $tmp1 if( defined $tmp1 );
# ALLOW_SKIPPED_PROOFS: if 0, skipped proofs (@proof) are not allowed,
# otherwise yes note that git-cnfig does not allow underscore, while
# shell does not allow dash, so we keep it only alphanumeric.
my $allow_skipped_proofs = 1;
$tmp1 = get_mwiki_var("allowskippedproofs");
$allow_skipped_proofs = $tmp1 if( defined $tmp1 );
my @repo_path_dirs = File::Spec->splitdir ($cwd);
my $repo_name = $repo_path_dirs[$#repo_path_dirs];
my $main_repo = $cwd;
my $compiled = $cwd . "/" . "../compiled";
my $sandbox = $cwd . "/" . "../sandbox";
# don't use this for coq
# my $sandbox_lib = $sandbox . "/" . "lib";
# TODO: does Coq need any settings?
# Set MIZFILES appropriately
#mizar::set_MIZFILES ($main_repo);
sub clean_the_dirty_sandbox {
my $rsync_output = `rsync -a --del $compiled/ $sandbox 2>&1`;
my $rsync_exit_code = ($? >> 8);
unless ($rsync_exit_code == 0) {
pc_print ("rsync did not exit cleanly when cleaning the dirty sandbox: $!");
pc_print ("It's output was:");
pc_print ("$rsync_output\n");
pc_print ("We cannot continue.");
exit 1;
}
}
# don't use for coq
# sub separate_lib_from_non_lib {
# foreach my $edited (@art_changed) {
# chomp ($edited);
# my ($name, $path, $extension) = fileparse ($edited, qr/\.[^.]+/);
# if ($path=~ m/^lib\//) {
# push (@lib_changed, $name);
# } else {
# pc_print ("You're committing an article ($edited) outside the lib subdirectory; we don'handle this case yet");
# exit 1;
# }
# }
# }
@lib_changed = @art_changed;
sub copy_new_articles_to_sandbox {
foreach my $article (@lib_changed) {
my $real_article_path = "$cwd/$article";
chomp($real_article_path);
my $sandbox_article_path = "$sandbox/$article";
chomp($sandbox_article_path);
($article =~ /^([A-Za-z0-9_]+\/([A-Za-z0-9_\/]+\/)*)[A-Za-z0-9_]+[.]$article_ext$/) or
die("Wrong file name: $article");
my $possibly_new_dir_path = $1;
`mkdir -p $sandbox/$possibly_new_dir_path`;
copy ($real_article_path, $sandbox_article_path)
or die ("You can't copy $real_article_path to $sandbox_article_path!");
}
}
# Set up PATH and MIZBIN
# if (!defined ($ENV{"MIZBIN"}) or -z $ENV{"MIZBIN"}) {
# $ENV{"MIZBIN"} = $sandbox . "/bin";
# }
# $ENV{"PATH"} = $ENV{"PATH"} . ":" . $ENV{"MIZBIN"};
# Set up PATH and COQBIN
if (!defined ($ENV{"COQBIN"}) or -z $ENV{"COQBIN"}) {
$ENV{"COQBIN"} = $sandbox . "/bin";
}
$ENV{"PATH"} = $ENV{"COQBIN"} . ":" . $ENV{"PATH"};
# separate_lib_from_non_lib ();
clean_the_dirty_sandbox ();
copy_new_articles_to_sandbox ();
sub ensure_existence {
my $path = shift;
if (-e $path) {
return $path;
} else {
die "There's nothing at $path, I'm afraid";
}
}
sub ensure_directory {
my $path = shift;
if (-d $path) {
return $path;
} else {
die "$path isn't a directory, I'm afraid";
}
}
# should go into the mizar lib
# sub explain_mizar_err_file {
# my $err_file_path = ensure_existence (shift);
# my $err_file_basename = `basename $err_file_path`;
# chomp $err_file_basename;
# my $explanation = '';
# my $err_file_fh;
# my @errors = ();
# open $err_file_fh, q{<}, $err_file_path
# or die ("Unable to open input filehandle for $err_file_path: $!");
# while (defined (my $error_file_line = <$err_file_fh>)) {
# chomp $error_file_line;
# push @errors, $error_file_line;
# }
# close $err_file_fh;
# foreach my $error (@errors) {
# my ($line, $column, $code) = split (/\ /, $error);
# unless (defined $line && defined $column && defined $code) {
# die ("The error file line \"$error\" has an unexpected format");
# }
# $explanation .= pc_pad ("[$err_file_basename]: line $line, column $column: "
# . mizar::lookup_error_code ($code));
# }
# return $explanation;
# }
# not used for Coq I guess
# sub explain_err_files_in_directory {
# my $dir = ensure_directory (shift);
# my $explanation = '';
# my @non_trivial_err_files
# = `find $dir -type f -name "*\.err" -not -size 0 | xargs basename`;
# if (scalar @non_trivial_err_files == 0) {
# $explanation .= pc_pad ("No error files were generated by the mizar tools.");
# } else {
# $explanation .= pc_pad ("Summary of the errors in the mizar code:");
# $explanation
# .= pc_pad ("************************************************************\n");
# foreach my $non_trivial_err_file (@non_trivial_err_files) {
# chomp $non_trivial_err_file;
# my $err_file_path = $dir . "/" . $non_trivial_err_file;
# $explanation .= pc_pad (explain_mizar_err_file ($err_file_path));
# $explanation
# .= pc_pad ("************************************************************\n");
# }
# }
# return $explanation;
# }
sub explain_make_errors {
my $dir = ensure_directory (shift);
my $error_file_to_test = ensure_existence (shift);
my $error_msg = shift;
my $explanation = '';
$explanation .= pc_pad ("$error_msg");
$explanation .= pc_pad ("The output of the build procedure was:");
$explanation .= pc_pad ("============================================================");
open my $err_fh, q{<}, $error_file_to_test;
while (defined (my $err_line = <$err_fh>)) {
$explanation .= pc_pad ($err_line);
}
close $err_fh
or die "Unable to close the input filehandle for $error_file_to_test! $!";
$explanation .= pc_pad ("============================================================");
# $explanation .= explain_err_files_in_directory ($dir);
return $explanation;
}
sub maybe_die_if_make_errors_in_dir {
my $dir = ensure_directory (shift);
my $error_file = ensure_existence (shift);
my $error_message = shift;
unless (-z $error_file) {
pc_print (explain_make_errors ($dir, $error_file, $error_message));
pc_print ('Your changes are inadmissible.');
exit 1;
}
return;
}
sub die_if_make_died {
my $exit_code = shift;
unless ($exit_code == 0) {
pc_print ("The build procedure did not exit cleanly! (exit code exit_code)\n");
exit 1;
}
return;
}
# Now try to verify the new articles
chdir ($sandbox);
system ("make --jobs $makejobs allvo 2> make-vrf-err | tee make-vrf-out");
# die_if_make_died ($? >> 8);
maybe_die_if_make_errors_in_dir ($sandbox, "$sandbox/make-vrf-err",
'Failure verifying ');
# Ensure that the new articles do not have any "@proof" (for Mizar) or "Admit(ted)" for Coq bits.
# we do not do this check for Coq now - too limiting for developers.
my $mizar_skip_proof_regexp = '\@proof';
my $coq_skip_proof_regexp = '\bAdmit\(ted\)\b';
my $skip_proof_regexp = $coq_skip_proof_regexp;
## TODO: this does not work for Coq because of Coq comments
if ($allow_skipped_proofs == 0)
{
chdir ($sandbox);
foreach my $article_full (@lib_changed)
{
if (system ("grep '$skip_proof_regexp' $article_full | grep --invert-match --max-count=1 '::'") == 0)
{
pc_print ("You are not allowed to omit proofs from articles in the library.");
exit 1;
}
}
}
pc_print ("Your changes are admissible\n");
exit 0; # i.e., we made it -- phew!