Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Python script for dealing with deprecated notations in Coq
#!/usr/bin/env python3
import sys, re, os
from collections import defaultdict
# Authors: Jason Gross and Jean-Christophe Léchenet
# Usage: ./ 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
# ./ 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
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:
warning1 ='File "([^"]*)", line ([0-9]*), characters ([0-9]*)-([0-9]*):', line)
if not warning1:
line = fin.readline ()
# the "[compatibility-notation,deprecated]" part may be rejected
# to a third line
warning2 ='Warning: ([^ ]*)\s+is\s+([^ ]*)(?:\n|\s*.compatibility-notation,deprecated.)', line)
if not warning2:
filename =
line =
old_notation =
new_notation =
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(
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]):
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
You can’t perform that action at this time.