From 1cba5b1fce36edfe731a7890569fd13525d7e9c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 14 Nov 2023 15:22:53 +0000 Subject: [PATCH] remove unused scripts --- Dockerfile | 39 -------------------------- scripts/detect_errors.py | 51 ---------------------------------- scripts/fetch_olean_cache.sh | 53 ------------------------------------ scripts/get_cache.sh | 23 ---------------- scripts/mk_all.sh | 4 +-- scripts/nolints.txt | 2 -- scripts/update_nolints.sh | 13 --------- 7 files changed, 2 insertions(+), 183 deletions(-) delete mode 100644 Dockerfile delete mode 100644 scripts/detect_errors.py delete mode 100644 scripts/fetch_olean_cache.sh delete mode 100755 scripts/get_cache.sh delete mode 100644 scripts/nolints.txt delete mode 100644 scripts/update_nolints.sh diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index fafda68a3fa..00000000000 --- a/Dockerfile +++ /dev/null @@ -1,39 +0,0 @@ -FROM texlive/texlive:latest - -# Install Python 3.10 -WORKDIR /py -RUN apt update && apt install -y build-essential zlib1g-dev libncurses5-dev \ - libgdbm-dev libnss3-dev libssl-dev libreadline-dev libffi-dev \ - libsqlite3-dev wget libbz2-dev liblzma-dev -RUN apt upgrade -y -RUN wget https://www.python.org/ftp/python/3.10.0/Python-3.10.0.tgz -RUN tar -xf Python-3.10.*.tgz -WORKDIR /py/Python-3.10.0 -RUN ./configure -RUN make -RUN make altinstall -WORKDIR / - -# Install blueprint dependencies -RUN python3.10 -m pip install mathlibtools invoke -RUN apt install graphviz libgraphviz-dev pandoc -y -RUN git clone https://github.com/plastex/plastex.git -RUN python3.10 -m pip install ./plastex -RUN rm -rf ./plastex -RUN git clone https://github.com/PatrickMassot/leanblueprint.git -RUN python3.10 -m pip install ./leanblueprint -RUN rm -rf ./leanblueprint - -# Install doc-gen -RUN git clone https://github.com/leanprover-community/doc-gen.git -RUN python3.10 -m pip install -r ./doc-gen/requirements.txt -RUN rm -rf ./doc-gen - -# Install lean -RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \ - | sh -s -- --default-toolchain none -y - -WORKDIR /src - -# Run the continuous integration pipeline -ENTRYPOINT inv ci diff --git a/scripts/detect_errors.py b/scripts/detect_errors.py deleted file mode 100644 index 3d8b4dbfb14..00000000000 --- a/scripts/detect_errors.py +++ /dev/null @@ -1,51 +0,0 @@ -import itertools -from json import loads -from pathlib import Path -import sys - -def encode_msg_text_for_github(msg): - # even though this is probably url quoting, we match the implementation at - # https://github.com/actions/toolkit/blob/af821474235d3c5e1f49cee7c6cf636abb0874c4/packages/core/src/command.ts#L36-L94 - return msg.replace('%', '%25').replace('\r', '%0D').replace('\n', '%0A') - -def format_msg(msg): - # Formatted for https://github.com/actions/toolkit/blob/master/docs/commands.md#log-level - - # mapping between lean severity levels and github levels. - # github does not support info levels, which are emitted by `#check` etc: - # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-a-debug-message - severity_map = {'information': 'warning'} - severity = msg.get('severity') - severity = severity_map.get(severity, severity) - - # We include the filename / line number information as both message and metadata, to ensure - # that github shows it. - msg_text = f"{msg['file_name']}:{msg.get('pos_line')}:{msg.get('pos_col')}:\n{msg.get('text')}" - msg_text = encode_msg_text_for_github(msg_text) - return f"::{severity} file={msg['file_name']},line={msg.get('pos_line')},col={msg.get('pos_col')}::{msg_text}" - -def write_and_print_noisy_files(noisy_files): - with open('src/.noisy_files', 'w') as f: - for file in noisy_files: - f.write(file + '\n') - print(file) - -noisy_files = set() -for line in sys.stdin: - msg = loads(line) - print(format_msg(msg)) - if msg.get('severity') == 'error': - if len(noisy_files) > 0: - print("Also, the following files were noisy:") - write_and_print_noisy_files(noisy_files) - sys.exit(1) - elif msg.get('text', '').endswith("uses sorry"): - # Using sorry should not cause the build to fail in this repository. - continue - else: - noisy_files.add(str(Path(msg['file_name']).relative_to(Path.cwd()))) - -if len(noisy_files) > 0: - print("Build succeeded, but the following files were noisy:") - write_and_print_noisy_files(noisy_files) - sys.exit(1) \ No newline at end of file diff --git a/scripts/fetch_olean_cache.sh b/scripts/fetch_olean_cache.sh deleted file mode 100644 index c31fb0ee2a8..00000000000 --- a/scripts/fetch_olean_cache.sh +++ /dev/null @@ -1,53 +0,0 @@ -#!/usr/bin/env bash -set -e -set -x - -archive_url=$(grep -E "^olean_url" ./leanpkg.toml | sed "s/.*=\s*['\"]\(.*\)['\"]/\1/") -if [[ -z $archive_url ]]; then - # Currently, it doesn't make sense to store the field in leanpkg.toml since leanproject/leanpkg - # will delete it, so hard code it here instead. - archive_url="https://oleanstorage.azureedge.net/mathlib/LeanCamCombi/" -fi -echo "olean cache location: $archive_url" - -# GIT_HISTORY_DEPTH is set in .github/workflows/build.yml -for new_git_sha in $(git log -${GIT_HISTORY_DEPTH:-20} --first-parent --pretty=format:%H) -do - if curl -sfI "$archive_url$new_git_sha.tar.xz" ; then - echo "found ancestor Git sha: $new_git_sha" - break - fi - new_git_sha="" -done -# exit if there were no successful requests -[ "$new_git_sha" != "" ] || exit 0 - -# A list of directories containing .olean files. We are being conservative to -# avoid traversing irrelevant directories and affecting directories we do not -# want changed (e.g. $root/.git). -dirs="src" - -# if there are errors extracting the olean cache, delete all oleans and continue -(curl "$archive_url$new_git_sha.tar.xz" | tar xJ src) || { -find $dirs -name "*.olean" -delete || true -} - -# Delete every .olean where .lean appears in "src/.noisy_files" -if [ -e $dirs/.noisy_files ]; then - sed 's/\.lean$/.olean/' $dirs/.noisy_files | xargs -d'\n' rm -f - rm $dirs/.noisy_files -fi - -# Delete every .olean without a matching .lean. -# n.b. this for loop will break if there are filenames with spaces -for olean_file in `find $dirs -name "*.olean"` -do - lean_file=${olean_file%.olean}.lean - if [ ! -e $lean_file ]; then - rm $olean_file - fi -done - -# Delete all empty directories. An empty directory may have been created if it -# does not contain any .lean files and all of its .olean files were deleted. -find $dirs -type d -empty -delete diff --git a/scripts/get_cache.sh b/scripts/get_cache.sh deleted file mode 100755 index 3f44a11a5e9..00000000000 --- a/scripts/get_cache.sh +++ /dev/null @@ -1,23 +0,0 @@ -#!/usr/bin/env bash - -set -o errexit # Exit on most errors (see the manual) -set -o nounset # Disallow expansion of unset variables -set -o pipefail # Use last non-zero exit code in a pipeline - -if ! git rev-parse HEAD > /dev/null 2>&1; then - echo "Run this script from inside the git repository." - exit 1 -fi - -cd $(git rev-parse --show-toplevel) -lake exe cache get - -echo "Trying to download project cache" -if wget https://oleanstorage.azureedge.net/mathlib/LeanCamCombi/"$(git rev-parse HEAD)".tar.xz 2> /dev/null; then - echo "Found oleans at https://oleanstorage.azureedge.net/mathlib/LeanCamCombi/" - tar -xf "$(git rev-parse HEAD)".tar.xz - rm "$(git rev-parse HEAD)".tar.xz - echo "Extracted oleans into src and deleted archive" -else - echo "No olean cache available" -fi diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh index e7ace100849..4b6033fb000 100755 --- a/scripts/mk_all.sh +++ b/scripts/mk_all.sh @@ -6,8 +6,8 @@ # ./scripts/mk_all.sh data/real # ./scripts/mk_all.sh ../archive # -# Makes a mathlib/src/$directory/all.lean importing all files inside $directory. -# If $directory is omitted, creates `mathlib/src/all.lean`. +# Makes a $directory/../$directory.lean file importing all files inside $directory. +# If $directory is omitted, creates `LeanCamCombi.lean`. cd "$( dirname "${BASH_SOURCE[0]}" )"/../LeanCamCombi if [[ $# = 1 ]]; then diff --git a/scripts/nolints.txt b/scripts/nolints.txt deleted file mode 100644 index 728975cc6ff..00000000000 --- a/scripts/nolints.txt +++ /dev/null @@ -1,2 +0,0 @@ -import .all -run_cmd tactic.skip diff --git a/scripts/update_nolints.sh b/scripts/update_nolints.sh deleted file mode 100644 index d62ad74efca..00000000000 --- a/scripts/update_nolints.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/usr/bin/env bash - -set -e -set -x - -# Exit if there are no changes relative to master -git diff-index --quiet refs/remotes/origin/master -- scripts/nolints.txt && exit 0 - -git checkout master -git add scripts/nolints.txt -git commit -m "chore(scripts): update nolints.txt" -git pull origin master || exit 0 -git push origin master \ No newline at end of file