From ab6b1b49185b2bd538ba486466cde58988a93766 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 14 Oct 2020 19:14:00 +0200 Subject: [PATCH] chore: delete obsolete scripts --- script/check_md_links.py | 84 ---------------------------- script/demangle_cpptype.py | 53 ------------------ script/dropbox_upload.py | 109 ------------------------------------- script/lcov.sh | 16 ------ script/lib_perf.sh | 20 ------- script/port.pl | 104 ----------------------------------- script/port.txt | 43 --------------- script/run_tests.sh | 4 -- script/server_test.py | 25 --------- 9 files changed, 458 deletions(-) delete mode 100755 script/check_md_links.py delete mode 100755 script/demangle_cpptype.py delete mode 100755 script/dropbox_upload.py delete mode 100755 script/lcov.sh delete mode 100755 script/lib_perf.sh delete mode 100755 script/port.pl delete mode 100644 script/port.txt delete mode 100755 script/run_tests.sh delete mode 100755 script/server_test.py diff --git a/script/check_md_links.py b/script/check_md_links.py deleted file mode 100755 index 2d81c1b665..0000000000 --- a/script/check_md_links.py +++ /dev/null @@ -1,84 +0,0 @@ -#!/usr/bin/env python -# -*- coding: utf-8 -*- -# -# Copyright (c) 2016 Sebastian Ullrich. All rights reserved. -# Released under Apache 2.0 license as described in the file LICENSE. -# -# Author: Sebastian Ullrich -# -# Python 2/3 compatibility -from __future__ import print_function - -import argparse -import collections -import os -import sys -try: - from urllib.request import urlopen - from urllib.parse import urlparse -except ImportError: - from urlparse import urlparse - from urllib import urlopen -try: - import mistune -except ImportError: - print("Mistune package not found. Install e.g. via `pip install mistune`.") - -parser = argparse.ArgumentParser(description="Check all *.md files of the current directory's subtree for broken links.") -parser.add_argument('--http', help="also check external links (can be slow)", action='store_true') -parser.add_argument('--check-missing', help="also find unreferenced lean files", action='store_true') -args = parser.parse_args() - -lean_root = os.path.join(os.path.dirname(__file__), os.path.pardir) -lean_root = os.path.normpath(lean_root) -result = {} - -def check_link(link, root): - if link.startswith('http'): - if not args.http: - return True - if link not in result: - try: - urllib.request.urlopen(link) - result[link] = True - except: - result[link] = False - return result[link] - else: - if link.startswith('/'): - # project root-relative link - path = lean_root + link - else: - path = os.path.join(root, link) - - path = os.path.normpath(path) # should make it work on Windows - - result[path] = os.path.exists(path) - return result[path] - -# check all .md files -for root, _, files in os.walk('.'): - for f in files: - if not f.endswith('.md'): - continue - - path = os.path.join(root, f) - - class CheckLinks(mistune.Renderer): - def link(self, link, title, content): - if not check_link(link, root): - print("Broken link", link, "in file", path) - - mistune.Markdown(renderer=CheckLinks())(open(path).read()) - -if args.check_missing: - # check all .(h)lean files - for root, _, files in os.walk('.'): - for f in files: - path = os.path.normpath(os.path.join(root, f)) - if (path.endswith('.lean') or path.endswith('.hlean')) and path not in result: - result[path] = False - print("Missing file", path) - -if not all(result.values()): - sys.exit(1) diff --git a/script/demangle_cpptype.py b/script/demangle_cpptype.py deleted file mode 100755 index fa67ae703e..0000000000 --- a/script/demangle_cpptype.py +++ /dev/null @@ -1,53 +0,0 @@ -#!/usr/bin/env python -# -# Copyright (c) 2013 Microsoft Corporation. All rights reserved. -# Released under Apache 2.0 license as described in the file LICENSE. -# -# Author: Soonho Kong -# -# What's this? -# ============ -# It takes an input from stdin and demangle c++ type if the line -# matches the following patten: -# -# .* : := .* -# -# which, is the format that we are using in lean_assert. -# -# It calls "c++filt" to do the work. -# - -# Python 2/3 compatibility -from __future__ import print_function - -import re -import sys -import subprocess -import fileinput - -pattern_str = "(.* : )([A-Za-z0-9]+)( := .*)" -pattern = re.compile(pattern_str) -cppfilt = "c++filt" -cppfilt_option = "--types" - -def process_line(line): - result = pattern.match(line); - if result == None: - print(line, end=' ') - else: - p = subprocess.Popen(cppfilt + " " + cppfilt_option + " " + result.group(2), - shell=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - ty = p.stdout.readlines()[0].strip() - retval= p.wait() - new_str = re.sub(pattern_str, r"\1" + ty + r"\3", line); - print(new_str, end=' ') - -if len(sys.argv) > 1: - for line in fileinput.input(): - process_line(line) -else: - while True: - line = sys.stdin.readline() - if not line: - break - process_line(line) diff --git a/script/dropbox_upload.py b/script/dropbox_upload.py deleted file mode 100755 index ad354e7054..0000000000 --- a/script/dropbox_upload.py +++ /dev/null @@ -1,109 +0,0 @@ -#!/usr/bin/env python -# -# Copyright (c) 2013 Microsoft Corporation. All rights reserved. -# Released under Apache 2.0 license as described in the file LICENSE. -# -# Author: Soonho Kong -# - -# Python 2/3 compatibility -from __future__ import print_function - -import dropbox -import os -import argparse - -parser = argparse.ArgumentParser() -parser.add_argument('--dropbox-token', type=str, help='Dropbox token for authentication', required=True) -parser.add_argument('--destpath', type=str, help='Destination in Dropbox', required=True) -parser.add_argument('--srcpath', type=str, help='Local directory to copy') -parser.add_argument('--copylist', type=str, help='File containing a list of files to copy') -parser.add_argument('--deletelist', type=str, help='File containing a list of files to delete') -args = parser.parse_args() - -if not args.srcpath and not args.copylist and not args.deletelist: - print("You need to specify one of the following options:") - print(" --srcpath,") - print(" --copylist,") - print(" --deletelist") - exit(1) - -access_token = args.dropbox_token -server_path = args.destpath - -# Connect DROPBOX -try: - client = dropbox.client.DropboxClient(access_token) - client.account_info() -except: - print("Failed to connect to Dropbox. Please check the access token.") - exit(1) - -count = 0 -def copy_file_with_retry(fullpath, targetpath, max_try): - global count - print("==> " + targetpath) - try: - handle = open(fullpath) - except: - print("FAILED: " + fullpath + " not found") - return - - try: - response = client.put_file(targetpath, handle, True) - except: - handle.close() - print("FAILED: " + targetpath) - if count < max_try: - count = count + 1 - copy_file_with_retry(fullpath, targetpath, max_try) - else: - raise - count = 0 - handle.close() - -def upload_dir_to_dropbox(localDir, serverDir): - localDir = os.path.expanduser(localDir) - for dirName, subdirList, fileList in os.walk(localDir): - for fname in fileList: - fullpath = os.path.normpath(dirName + "/" + fname) - targetpath = os.path.normpath(serverDir + "/" + fullpath[len(localDir):]) - copy_file_with_retry(fullpath, targetpath, 5) - -def remove_from_dropbox(p): - try: - client.file_delete(p) - print (p + " deleted from Dropbox") - except dropbox.rest.ErrorResponse: - print (p + " not exists") - -if args.srcpath: - local_path = args.srcpath - print ("Copy: " + local_path + " ==> " + server_path) - upload_dir_to_dropbox(local_path, server_path) - exit(0) - -if args.copylist: - copylist = args.copylist - print ("Copy files in " + copylist + " ==> " + server_path) - try: - copylist_handle = open(copylist, "r") - except IOError: - print('Failed to open ' + copylist) - for line in copylist_handle: - fullpath = os.path.normpath(line.strip()) - copy_file_with_retry(fullpath, os.path.normpath(server_path + "/" + fullpath), 5) - exit(0) - -if args.deletelist: - deletelist = args.deletelist - print ("Delete files in " + deletelist + " from Dropbox " + server_path) - try: - deletelist_handle = open(deletelist, "r") - except IOError: - print('Failed to open ' + deletelist) - deletelist_handle = open(deletelist, "r") - for line in deletelist_handle: - fullpath = os.path.normpath(line.strip()) - remove_from_dropbox(os.path.normpath(server_path + "/" + fullpath)) - exit(0) diff --git a/script/lcov.sh b/script/lcov.sh deleted file mode 100755 index c0707c9d8c..0000000000 --- a/script/lcov.sh +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/bash -CXX=$1 -GCOV_TOOL=$2 -LCOV=~/bin/lcov -GENHTML=~/bin/genhtml - -rm -rf build -mkdir -p build/testcov -cd build/testcov -cmake -DCMAKE_BUILD_TYPE=TESTCOV -DCMAKE_CXX_COMPILER="$CXX" ../../src -make -ctest -"$LCOV" -c -b ../../src -d . -o cov.info --no-external --gcov-tool "$GCOV_TOOL" -"$LCOV" --remove cov.info "tests/*" -o cov.info -"$GENHTML" cov.info --output-directory lcov -cd ../../ diff --git a/script/lib_perf.sh b/script/lib_perf.sh deleted file mode 100755 index 47b5d8c1fc..0000000000 --- a/script/lib_perf.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/bin/bash -# Script for collecting compilation times for the standard library -# It assumes the lean binary is at the bin directory -# It assumes the programs time and realpath are available -set -eu -TIME=/usr/bin/time -REALPATH=realpath - -if ! command -v $TIME 2> /dev/null > /dev/null; then - TIME=gtime -fi - -MY_PATH="`dirname \"$0\"`" -LEAN=$MY_PATH/../bin/lean -LIB=$MY_PATH/../library -for f in `find $LIB -name '*.lean'`; do - rf=`$REALPATH $f` - cp $rf tmp.lean - $TIME --format="$rf %e" $LEAN -j 0 tmp.lean > /dev/null -done diff --git a/script/port.pl b/script/port.pl deleted file mode 100755 index 69ed1edb22..0000000000 --- a/script/port.pl +++ /dev/null @@ -1,104 +0,0 @@ -#!/usr/bin/env perl - -# SEE ALSO THE DOCUMENTATION IN port.sh -# -# This perl script is for porting files from the standard library to the HoTT library -# -# To use: first make it executable (chmod u+x port.pl). Then type -# -# ./port.pl ../library/path/to/source.lean ../hott/path/to/destination.hlean ["from1" "to1" "from2" "to2" ...] -# -# This will port the file ../library/path/to/source.lean to ../hott/path/to/destination.hlean -# renaming core definitions form the standard library to core definitions in the HoTT library. -# These renamings are specified in port.txt. See the documentation in rename.pl for the syntax. -# The arguments "fromi" and "toi" are optional, but should be provided in pairs. -# These arguments will replace "fromi" by "toi" in the specified file, -# before doing any other renamings. -# -# We use slightly different regular expressions here. Given the replacement rule foo:bar, we replace -# foo by bar except is foo is preceded or followed by a letter. We still replace foo if it's -# followed by a digit, underscore, period or similar. -# -# TODO: Currently we use dictionaries to store the renamings. This has the unfortunate consequence -# that we cannot control the order in which the substitutions happens. This makes it very hard to -# replace all occurrences of "and" by "prod", but all occurrences of "and.intro" by "prod.mk" - -use strict; -use warnings; -use Cwd 'abs_path'; -use File::Basename; -use File::Spec::Functions; -use File::Copy; -use feature 'unicode_strings'; - -# the global list of renamings -my %renamings = (); -my %literalrenamings = (); -my %literalrenamings2 = (); - -# get the list of renamings from the file -sub get_renamings { - if (scalar(@ARGV)%2==1) {die "ERROR: odd number of arguments provided"} - %literalrenamings2 = @ARGV; - my $fullname = catfile(dirname(abs_path($0)), "port.txt"); - open (my $renaming_file, "<", $fullname) or die $!; - while (<$renaming_file>) { - if (/([\w'.]+)[:]([\w'.]+)\n/) { - $renamings{$1} = $2; - } elsif (/(.+)[;](.+)\n/) { - $literalrenamings{$1} = $2; - } - } - close $renaming_file or die $!; -} - -# print them out - for debugging -sub show_renamings { - foreach my $key (keys %renamings) { - print $key, " => ", $renamings{$key}, "\n"; - } - print "\n"; - foreach my $lkey (keys %literalrenamings2) { - print $lkey, " -> ", $literalrenamings2{$lkey}, "\n"; - } - foreach my $lkey (keys %literalrenamings) { - print $lkey, " -> ", $literalrenamings{$lkey}, "\n"; - } -} - -# rename all identifiers a file; original goes in file.orig -sub rename_in_file { - my $filename = shift; - local($^I, @ARGV) = ('.temp', $filename); - while (<>) { - foreach my $lkey (keys %literalrenamings2) { - # replace all instances of lkey - # if (/$lkey/) {print STDOUT "renamed ", $lkey, "\n"; } - s/$lkey/$literalrenamings2{$lkey}/g; - } - foreach my $key (keys %renamings) { - # replace instances of key, not preceeded by a letter, and not - # followed by a letter, number, or ' - s/(?