Turn QED's in a Coq development into Defined's. Useful for when you need to compute on proofs but they've been QED'd.

transparify.rb

# script to transform all theorems in all Coq files
# in the given directory's tree
# such that Qed's become Defined's.

loc = ARGV.first
ldir = Dir.open loc

$vfiles = []

# where is the directory to look
# recursively accumulates all .v files, skipping symlinks
def acc_vfiles(where)
  where.each { |file|
    if File.directory? file
    then
      if not File.symlink? file and
        file != '.' and file != '..'
      then
        acc_vfiles (Dir.open file)
      end
    else
      if /.*\.v\Z/.match file
        $vfiles << (File.expand_path file, where)
      end
    end
  }
end

acc_vfiles ldir

# transformation to apply to each file
def do_transform(file_loc)
  print "Doing transform on ", file_loc, "\n"

  contents = File.read file_loc

  # the actual transformation
  regex = /(Theorem|Lemma|Fact|Remark|Corollary|Proposition)\s+(\S+)\s+:(((?!(Qed\.|Defined\.)).)*)Qed\./m

  new_contents = contents.gsub regex, "\\1 \\2 : \\3Defined. Opaque \\2."

  # print contents
  file = File.open file_loc, 'w'
  file.write new_contents
  file.close
end

# now that we have the files, we transform each one.
for file in $vfiles
  do_transform file
end

#do_transform("/home/mario/LocalCode/compcert-2.4/flocq/Appli/Fappli_IEEE.v")