chore: delete obsolete scripts
This commit is contained in:
Sebastian Ullrich
parent
c077363c43
commit
ab6b1b4918
9 changed files with 0 additions and 458 deletions
|
|
@ -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)
|
||||
|
|
@ -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:
|
||||
#
|
||||
# .* : <C++_TYPE> := .*
|
||||
#
|
||||
# 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)
|
||||
|
|
@ -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)
|
||||
|
|
@ -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 ../../
|
||||
|
|
@ -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
|
||||
104
script/port.pl
104
script/port.pl
|
|
@ -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/(?<![a-zA-Z])$key(?![a-zA-Z])/$renamings{$key}/g;
|
||||
}
|
||||
foreach my $lkey (keys %literalrenamings) {
|
||||
# replace all instances of lkey
|
||||
s/$lkey/$literalrenamings{$lkey}/g;
|
||||
}
|
||||
print;
|
||||
}
|
||||
}
|
||||
|
||||
my $oldfile = shift;
|
||||
my $newfile = shift;
|
||||
my $backup = "${newfile}.orig";
|
||||
if (-e $newfile) {
|
||||
print "backing up file ${newfile}.\n" unless -e $backup;
|
||||
copy($newfile,$backup) or die "Copy failed: $!" unless -e $backup ;
|
||||
}
|
||||
print "porting ", $oldfile, " to ",$newfile, ".\n";
|
||||
copy($oldfile,$newfile) or die "Copy failed: $!";
|
||||
get_renamings;
|
||||
# show_renamings;
|
||||
rename_in_file $newfile;
|
||||
unlink "${newfile}.temp";
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
Prop:Type
|
||||
|
||||
true:unit
|
||||
trivial:star
|
||||
|
||||
false:empty
|
||||
|
||||
induction_on:rec_on
|
||||
|
||||
∨;⊎
|
||||
or:sum
|
||||
sum.intro_left _;sum.inl
|
||||
sum.intro_right _;sum.inr
|
||||
|
||||
or.intro_left _;sum.inl
|
||||
or.intro_right _;sum.inr
|
||||
|
||||
∧;×
|
||||
and:prod
|
||||
|
||||
and.intro:pair
|
||||
and.elim_left:prod.pr1
|
||||
and.left:prod.pr1
|
||||
and.elim_right:prod.pr2
|
||||
and.right:prod.pr2
|
||||
|
||||
prod.intro:pair
|
||||
prod.elim_left:prod.pr1
|
||||
prod.left:prod.pr1
|
||||
prod.elim_right:prod.pr2
|
||||
prod.right:prod.pr2
|
||||
|
||||
|
||||
∀;Π
|
||||
|
||||
∃;Σ
|
||||
exists.intro:sigma.mk
|
||||
exists.elim:sigma.rec_on
|
||||
Exists.rec:sigma.rec
|
||||
|
||||
eq.symm:inverse
|
||||
congr_arg:ap
|
||||
eq.substr;tr_rev _
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
ctest -D ExperimentalBuild
|
||||
yes "C" | ctest -VV
|
||||
exit 0
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
#!/usr/bin/env python3
|
||||
#
|
||||
# Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
# Released under Apache 2.0 license as described in the file LICENSE.
|
||||
#
|
||||
# Author: Gabriel Ebner
|
||||
#
|
||||
|
||||
import sys, subprocess, json, time
|
||||
|
||||
_, file_name = sys.argv
|
||||
|
||||
proc = subprocess.Popen(["lean", "--server"],
|
||||
stdin=subprocess.PIPE, stdout=subprocess.PIPE,
|
||||
universal_newlines=True, bufsize=1)
|
||||
|
||||
def send(req):
|
||||
proc.stdin.write(json.dumps(req) + "\n")
|
||||
print(proc.stdout.readline().rstrip())
|
||||
|
||||
while True:
|
||||
content = open(file_name).read()
|
||||
send({ 'command': 'sync', 'file_name': file_name, 'content': content })
|
||||
send({ 'command': 'check' })
|
||||
time.sleep(1)
|
||||
Loading…
Add table
Reference in a new issue