Last active
May 6, 2020 13:37
-
-
Save JasonGross/9770653967de3679d131c59d42de6d17 to your computer and use it in GitHub Desktop.
Python script for dealing with deprecated notations in Coq
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python3 | |
import sys, re, os | |
from collections import defaultdict | |
# Authors: Jason Gross and Jean-Christophe Léchenet | |
# | |
# Usage: ./replace-notations.py logfile | |
# Uses the warnings in logfile to locate compatibility notation warnings, | |
# then search and replace to use the correct notations. | |
# | |
# Extended Usage: | |
# First, using the old version of Coq (e.g., 8.9), which emits deprecation | |
# warnings, run something like | |
# make -Okj 2>&1 | tee logfile | |
# You may want to first run `make clean` to ensure that all files get built. | |
# N.B. The -O is for --output-sync, which ensures that output is interwoven | |
# correctly when running with -j | |
# | |
# Once the build completes, you can run | |
# ./replace-notations.py logfile | |
# This will update the .v files in place. After this, you will want to run | |
# `make clean; make` with the *new* version of Coq (e.g., master, 8.10), | |
# which does not support compatbility notations, or else you will want to run | |
# `make OTHERFLAGS='-w "+compatibility-notation"'` with the old version of Coq. | |
# | |
# Note that in rare cases, there may be some compatibility notation uses that are | |
# not correctly updated by this script, and which have to be updated by hand. | |
# | |
# From https://github.com/coq/coq/issues/8383#issuecomment-424525941 | |
if __name__ == '__main__': | |
if len(sys.argv) <= 1: | |
print("Add a log file to the command line", file=sys.stderr) | |
exit (-1) | |
logfile = sys.argv[1] | |
# process warnings one by one | |
repl = defaultdict(list) | |
with open(logfile) as fin: | |
while True: | |
# search for a line of the form "File ..." followed by another | |
# line of the form "Warning ..." | |
line = fin.readline() | |
if not line: | |
break | |
warning1 = re.search(r'File "([^"]*)", line ([0-9]*), characters ([0-9]*)-([0-9]*):', line) | |
if not warning1: | |
continue | |
line = fin.readline () | |
# the "[compatibility-notation,deprecated]" part may be rejected | |
# to a third line | |
warning2 = re.search(r'Warning: ([^ ]*)\s+is\s+([^ ]*)(?:\n|\s*.compatibility-notation,deprecated.)', line) | |
if not warning2: | |
continue | |
filename = warning1.group(1) | |
line = warning1.group(2) | |
old_notation = warning2.group(1) | |
new_notation = warning2.group(2) | |
print('File {} at line {}: {} should be written {}.' | |
.format(filename, line,old_notation,new_notation)) | |
# line numbers are 1-indexed in Coq, 0-indexed in python | |
# character numbers are 0-indexed in both | |
numline = int(line) - 1 | |
last_char = int(warning1.group(4)) | |
repl[filename].append((numline, old_notation, new_notation, last_char)) | |
for filename, l in repl.items(): | |
# for each file, we correct warnings line by line | |
with open(filename, 'r') as vfile: | |
data = vfile.readlines() | |
for numline, old_notation, new_notation, last_char in l: | |
# When notation appears in multiline tactics, the line reported is | |
# the starting line of the tactic, thus the notation may | |
# be on a following line. In this case, though, the last character | |
# is greater than the length of the line, so we can detect it. | |
# When this occurs, we try to | |
# find the corresponding notation in the following lines. Cannot | |
# blindly rely on nb_sub = 0 to detect such cases, since, for some | |
# reason, some warnings appear twice (and here we perform as many | |
# substitutions as we can, we could try to perform at most one for | |
# each warning to be more precise). | |
while True: | |
data[numline], nb_sub = re.subn(r'\b{}\b'.format(old_notation), | |
new_notation, data[numline]) | |
if nb_sub > 0 or last_char < len(data[numline]): | |
break | |
last_char -= len(data[numline]) | |
numline += 1 | |
assert (numline < len(data)) | |
with open(filename, 'w') as vfile: | |
vfile.writelines( data ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment