diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ee6d23c9fcc..5a9ac0206b4 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -89,7 +89,7 @@ jobs: # Install Python and friends for website generation only where needed - uses: actions/setup-python@v5 with: - python-version: '3.8' + python-version: '3.10' check-latest: true cache: 'pip' @@ -110,7 +110,7 @@ jobs: - uses: actions/setup-python@v5 with: - python-version: '3.8' + python-version: '3.10' check-latest: true cache: 'pip' diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml index aeb1face4cc..5741534d107 100644 --- a/.github/workflows/pages.yaml +++ b/.github/workflows/pages.yaml @@ -89,7 +89,7 @@ jobs: - uses: actions/setup-python@v5 with: - python-version: '3.8' + python-version: '3.10' check-latest: true cache: 'pip' diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index d123890ea36..2bf210ebe5e 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -2,16 +2,18 @@ fail_fast: false repos: - repo: https://github.com/pre-commit/pre-commit-hooks - rev: v3.2.0 + rev: v6.0.0 hooks: - id: trailing-whitespace - id: end-of-file-fixer - id: mixed-line-ending + # Behavior depends on the Python version you're running with, + # there's no way to tell it to target a fixed minimum version # - id: double-quote-string-fixer - id: check-ast - id: check-yaml # - id: check-json # Doesn't accept json with comments - # - id: requirements-txt-fixer # Can't handle comments + - id: requirements-txt-fixer - repo: https://github.com/codespell-project/codespell rev: v2.4.1 @@ -114,21 +116,22 @@ repos: # types_or: [markdown, text] # require_serial: false + # Run these checks after files are generated by the rules above - repo: https://github.com/pre-commit/pre-commit-hooks - rev: v3.2.0 + rev: v6.0.0 hooks: - id: check-case-conflict - id: check-merge-conflict - # - repo: https://github.com/pre-commit/mirrors-autopep8 - # rev: 'v2.0.2' - # hooks: - # - id: autopep8 - # name: Python scripts formatting - # args: ['-i', '--global-config', '/dev/null'] + - repo: https://github.com/hhatto/autopep8 + rev: 'v2.3.2' + hooks: + - id: autopep8 + name: Python scripts formatting + args: ['-i', '--global-config', '/dev/null'] - repo: https://github.com/pre-commit/mirrors-prettier - rev: 'v3.0.0-alpha.6' + rev: 'v4.0.0-alpha.8' hooks: - id: prettier name: CSS, JS, YAML and Markdown (no codeblocks) formatting diff --git a/docs/CODINGSTYLE.md b/docs/CODINGSTYLE.md index b753b16f317..14b874c74ff 100644 --- a/docs/CODINGSTYLE.md +++ b/docs/CODINGSTYLE.md @@ -110,7 +110,6 @@ agda-unimath project. definition. This contradicts our objective of organizing the library into compact, reusable components. If a `where` block is deemed necessary, follow these conventions: - - Opt for `where` blocks over `let` expressions. - Indent the `where` keyword by two spaces and align their content with the `where` keyword. @@ -136,7 +135,6 @@ agda-unimath project. There are multiple syntaxes for writing lambda expressions in Agda. Generally, you have the following options: - 1. Regular lambda expressions without pattern matching: ```agda @@ -402,7 +400,6 @@ library: - In order to improve the readability on the agda-unimath website, we use a standard line length of 80 characters. There are only a few exceptions that enable us to have names that are more than 80 characters long: - - Named `module` declarations - `open import` statements - Lines consisting of a single, possibly parenthesized (`(){}`), token that is diff --git a/docs/HOWTO-INSTALL.md b/docs/HOWTO-INSTALL.md index a366a9a5805..08b720f5877 100644 --- a/docs/HOWTO-INSTALL.md +++ b/docs/HOWTO-INSTALL.md @@ -20,9 +20,9 @@ In order to contribute to the agda-unimath library you will additionally need: 1. `git` 2. `make` -3. `python` version 3.8 or newer -4. The python libraries `pre-commit`, `pybtex`, `requests`, `tomli`, and - `graphviz`. These can be installed by running +3. `python` version 3.10 or newer +4. The python libraries `pre-commit`, `pybtex`, `tomli`, and `graphviz`. These + can be installed by running ```shell python3 -m pip install -r scripts/requirements.txt ``` @@ -316,7 +316,7 @@ will need to install the `pre-commit` tool and the hooks' Python dependencies. The easiest way to accomplish this is by using the Python package manager `pip`. First, make sure that you have the latest version of Python and pip installed on -your computer; the hooks require Python 3.8 or newer. Then run the following +your computer; the hooks require Python 3.10 or newer. Then run the following command from the repository's main folder: ```shell @@ -392,7 +392,6 @@ This issue can arise if the `pre-commit` executable gets placed in the `ls ~/.local/bin | grep pre-commit` to see if the executable is present. 2. **Update your `PATH`**: - - If you're using the bash terminal, open your `.bashrc` file with a text editor like `nano`: @@ -409,7 +408,6 @@ This issue can arise if the `pre-commit` executable gets placed in the - Save the file and close the editor. 3. **Reload your `.bashrc`**: - - Run the following command to apply the changes: ```bash diff --git a/docs/MIXFIX-OPERATORS.md b/docs/MIXFIX-OPERATORS.md index 86bac14dd09..03d8e87d7b1 100644 --- a/docs/MIXFIX-OPERATORS.md +++ b/docs/MIXFIX-OPERATORS.md @@ -177,8 +177,8 @@ Below, we outline a list of general rules when assigning associativities. | 16 | Right homotopy whiskering `_·r_` | | 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, `_*_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` | | 10 | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad | -| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations | -| 5 | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_` | +| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations | +| 5 | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_` | | 3 | The pairing operators `_,_` and `_,ω_` | | 0-1 | Reasoning syntaxes | | -∞ | Function type formation `_→_` | diff --git a/flake.lock b/flake.lock index 433ef8c6517..769ef692340 100644 --- a/flake.lock +++ b/flake.lock @@ -71,29 +71,12 @@ "type": "github" } }, - "nixpkgs-python": { - "locked": { - "lastModified": 1720535198, - "narHash": "sha256-zwVvxrdIzralnSbcpghA92tWu2DV2lwv89xZc8MTrbg=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "205fd4226592cc83fd4c0885a3e4c9c400efabb5", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixos-23.11", - "repo": "nixpkgs", - "type": "github" - } - }, "root": { "inputs": { "flake-utils": "flake-utils", "mdbook-catppuccin": "mdbook-catppuccin", "nixpkgs": "nixpkgs", - "nixpkgs-mdbook": "nixpkgs-mdbook", - "nixpkgs-python": "nixpkgs-python" + "nixpkgs-mdbook": "nixpkgs-mdbook" } }, "systems": { diff --git a/flake.nix b/flake.nix index e1c0c7ab5b8..db4ecee1e74 100644 --- a/flake.nix +++ b/flake.nix @@ -5,10 +5,6 @@ # Unstable has Agda 2.8.0 nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; flake-utils.url = "github:numtide/flake-utils"; - # We aim to support Python 3.8 as long as Ubuntu 20.24 has LTS, - # since it ships with that version. Python 3.8 itself is already - # EOL, so it was dropped from nixpkgs 24.05 - nixpkgs-python.url = "github:NixOS/nixpkgs/nixos-23.11"; # Nixpkgs with tested versions of mdbook crates; # may be removed once we backport new mdbook assets to our # modified versions @@ -19,21 +15,25 @@ }; }; - outputs = { self, nixpkgs, nixpkgs-mdbook, nixpkgs-python, flake-utils, mdbook-catppuccin }: + outputs = { self, nixpkgs, nixpkgs-mdbook, flake-utils, mdbook-catppuccin }: flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages."${system}"; pkgs-mdbook = nixpkgs-mdbook.legacyPackages."${system}"; - pkgs-python = nixpkgs-python.legacyPackages."${system}"; - python = pkgs-python.python38.withPackages (p: with p; [ + # We aim to support Python 3.10 as long as Ubuntu 22.24 has LTS, + # since it ships with that version + python = pkgs.python310.withPackages (p: with p; [ # Keep in sync with scripts/requirements.txt # pre-commit <- not installed as a Python package but as a binary below pybtex - requests tomli graphviz ]); + # Make sure pre-commit also uses Python 3.10 + pre-commit = pkgs.pre-commit.override { + python3Packages = pkgs.python310Packages; + }; agda-unimath-package = { lib, mkDerivation, time }: mkDerivation { pname = "agda-unimath"; @@ -44,7 +44,7 @@ # We can reference the directory since we're using flakes, # which copies the version-tracked files into the nix store - # before evaluation, # so we don't run into the issue with + # before evaluation, so we don't run into the issue with # nonreproducible source paths as outlined here: # https://nix.dev/recipes/best-practices#reproducible-source-paths src = ./.; @@ -80,7 +80,7 @@ # maintenance scripts python # pre-commit checks - pkgs.pre-commit + pre-commit pkgs.nodejs ] ++ (with pkgs-mdbook; [ # working on the website diff --git a/scripts/generate_contributors.py b/scripts/generate_contributors.py index 0ef5b7aa5cf..d52ebd1fc04 100644 --- a/scripts/generate_contributors.py +++ b/scripts/generate_contributors.py @@ -44,8 +44,10 @@ def format_contributor(contributor): if __name__ == '__main__': parser = argparse.ArgumentParser( description='Generate contributors markdown content. Usage: generate_contributors.py ') - parser.add_argument('contributors_file', help='Path to the CONTRIBUTORS.toml file.') - parser.add_argument('output_file', help='Output file path to write the generated contributors markdown content to.') + parser.add_argument('contributors_file', + help='Path to the CONTRIBUTORS.toml file.') + parser.add_argument( + 'output_file', help='Output file path to write the generated contributors markdown content to.') args = parser.parse_args() contributors_data = parse_contributors_file(args.contributors_file) @@ -62,7 +64,8 @@ def format_contributor(contributor): git_log_output, contributors_data) if skipped_authors: - print_skipping_contributors_warning(skipped_authors, args.contributors_file) + print_skipping_contributors_warning( + skipped_authors, args.contributors_file) output = template.format( names='\n'.join((format_contributor(c) for c in sorted_authors)), @@ -71,7 +74,8 @@ def format_contributor(contributor): out_path = args.output_file if os.path.isdir(out_path): - print(f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr) + print( + f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr) sys.exit(2) parent = os.path.dirname(out_path) if parent: diff --git a/scripts/generate_dependency_graph_rendering.py b/scripts/generate_dependency_graph_rendering.py index 3816fdae210..ab95e0090b3 100644 --- a/scripts/generate_dependency_graph_rendering.py +++ b/scripts/generate_dependency_graph_rendering.py @@ -1,15 +1,25 @@ -import os import graphviz -import random +import json import math -import requests +import os +import random +import re +from urllib import request +from urllib.error import URLError from collections import defaultdict from utils import * import argparse -primes_hash_str = (19,2,1,7,5,3,11,13,17) -def hash_str(s) : - return sum(ord(char) * primes_hash_str[i%len(primes_hash_str)] for i,char in enumerate(s)) +primes_hash_str = (19, 2, 1, 7, 5, 3, 11, 13, 17) + +# This format is guaranteed by the GitHub documentation +# "The URL for the next page is followed by `rel="next"`" +NEXT_LINK_REGEX = re.compile(r'<([^>]+)> *; *rel="next"') + + +def hash_str(s): + return sum(ord(char) * primes_hash_str[i % len(primes_hash_str)] for i, char in enumerate(s)) + def find_agda_files(root_dir): """ @@ -22,74 +32,82 @@ def find_agda_files(root_dir): LABEL_COLORS_FALLBACK = { - "category-theory": "fbca04", - "commutative-algebra": "3577BB", - "domain-theory": "FCBFF5", - "elementary-number-theory": "4A6123", - "finite-algebra": "524F88", - "finite-group-theory": "9A01E2", - "foundation": "284530", - "globular-types": "4A7555", - "graph-theory": "CCC0C4", - "group-theory": "963872", - "higher-group-theory": "E79FEE", - "lists": "C9D999", - "literature": "3C3C0A", - "logic": "A9CFCE", - "metric-spaces": "923E82", - "modal-logic": "A4DC70", - "modal-type-theory": "E45F85", - "oeis": "F984EC", - "order-theory": "533A22", - "organic-chemistry": "07C851", - "orthogonal-factorization-systems": "578072", - "real-numbers": "B66877", - "reflection": "000000", - "ring-theory": "1A1277", - "set-theory": "98335C", - "simplicial-type-theory": "8C3F69", - "species": "EDA55F", - "structured-types": "069F6E", - "synthetic-category-theory": "2FEABE", - "synthetic-homotopy-theory": "B0D45A", - "trees": "0F1D69", - "type-theories": "610CCA", - "univalent-combinatorics": "F70D61", - "universal-algebra": "5467C3", - "wild-category-theory": "E2C12E", + 'category-theory': 'fbca04', + 'commutative-algebra': '3577BB', + 'domain-theory': 'FCBFF5', + 'elementary-number-theory': '4A6123', + 'finite-algebra': '524F88', + 'finite-group-theory': '9A01E2', + 'foundation': '284530', + 'globular-types': '4A7555', + 'graph-theory': 'CCC0C4', + 'group-theory': '963872', + 'higher-group-theory': 'E79FEE', + 'lists': 'C9D999', + 'literature': '3C3C0A', + 'logic': 'A9CFCE', + 'metric-spaces': '923E82', + 'modal-logic': 'A4DC70', + 'modal-type-theory': 'E45F85', + 'oeis': 'F984EC', + 'order-theory': '533A22', + 'organic-chemistry': '07C851', + 'orthogonal-factorization-systems': '578072', + 'real-numbers': 'B66877', + 'reflection': '000000', + 'ring-theory': '1A1277', + 'set-theory': '98335C', + 'simplicial-type-theory': '8C3F69', + 'species': 'EDA55F', + 'structured-types': '069F6E', + 'synthetic-category-theory': '2FEABE', + 'synthetic-homotopy-theory': 'B0D45A', + 'trees': '0F1D69', + 'type-theories': '610CCA', + 'univalent-combinatorics': 'F70D61', + 'universal-algebra': '5467C3', + 'wild-category-theory': 'E2C12E', } + def fetch_github_labels(repo): """Fetch labels and their colors from a GitHub repository.""" - url = f"https://api.github.com/repos/{repo}/labels" + url = f'https://api.github.com/repos/{repo}/labels' labels = {} try: while url: - response = requests.get(url) - response.raise_for_status() - page_labels = response.json() - labels.update({label['name']: label['color'] for label in page_labels}) + response = request.urlopen(url) + page_labels = json.loads(response.read()) + labels.update({label['name']: label['color'] + for label in page_labels}) + url = None + next_link_match = re.search( + NEXT_LINK_REGEX, response.headers.get('link', '')) # Check if there is a next page - url = response.links.get('next', {}).get('url') - except requests.RequestException as e: - eprint(f"Failed to fetch GitHub labels: {e}") + if next_link_match is not None: + url = next_link_match.group(1) + except URLError as e: + eprint(f'Failed to fetch GitHub labels: {e}') # Fallback to preloaded values return LABEL_COLORS_FALLBACK return labels + def module_based_color(module_name, label_colors): """Generate a color based on the module name using GitHub labels.""" for label, color in label_colors.items(): - if label == module_name or (label == "foundation" and module_name == "foundation-core"): - return f"#{color}" + if label == module_name or (label == 'foundation' and module_name == 'foundation-core'): + return f'#{color}' # Fallback to random color generation if no label matches base_color = (91, 155, 213) seed = hash_str(module_name) random.seed(seed) variation = [random.randint(-91, 70) for _ in range(3)] - new_color = tuple(min(255, max(0, base_color[i] + variation[i])) for i in range(3)) - return "#{:02X}{:02X}{:02X}".format(*new_color) + new_color = tuple( + min(255, max(0, base_color[i] + variation[i])) for i in range(3)) + return '#{:02X}{:02X}{:02X}'.format(*new_color) + def count_imports(graph): """Count the number of times each module is imported.""" @@ -99,6 +117,7 @@ def count_imports(graph): import_counts[dep] += 1 return import_counts + def build_dependency_graph(root_dir, most_imported_drop_count=20): """Construct a dependency graph from Agda files.""" graph = defaultdict(set) @@ -106,7 +125,8 @@ def build_dependency_graph(root_dir, most_imported_drop_count=20): agda_files = find_agda_files(root_dir) for file in agda_files: - module_name = os.path.splitext(os.path.relpath(file, root_dir))[0].replace(os.sep, ".") + module_name = os.path.splitext(os.path.relpath(file, root_dir))[ + 0].replace(os.sep, '.') module_name = module_name[:module_name.rfind('.')] imports = parse_agda_imports(file) graph[module_name].update(imports) @@ -117,12 +137,13 @@ def build_dependency_graph(root_dir, most_imported_drop_count=20): # Count imports and find top imported modules import_counts = count_imports(graph) - _top_imports = sorted(import_counts, key=import_counts.get, reverse=True)[:most_imported_drop_count] + _top_imports = sorted(import_counts, key=import_counts.get, reverse=True)[ + :most_imported_drop_count] top_imports = set(_top_imports) - eprint("Excluding modules:") + eprint('Excluding modules:') for i, m in enumerate(_top_imports): - eprint(f"{i+1:>3} ({import_counts[m]:>4} imports) {m}") + eprint(f'{i+1:>3} ({import_counts[m]:>4} imports) {m}') # Remove top modules from the graph for module in top_imports: @@ -133,62 +154,77 @@ def build_dependency_graph(root_dir, most_imported_drop_count=20): return graph, file_sizes + def generate_html_legend(label_colors, used_labels, output_file, label_counts): """Generate an HTML legend with used namespaces and their colors.""" - sorted_labels = sorted(used_labels, key=lambda label: label_counts.get(label, 0), reverse=True) + sorted_labels = sorted( + used_labels, key=lambda label: label_counts.get(label, 0), reverse=True) with open(output_file, 'w') as f: f.write('
\n') for label in sorted_labels: if label in label_colors: color = label_colors[label] - f.write(f' 
{label}
\n') + f.write( + f' 
{label}
\n') f.write('
\n') + def render_graph(graph, file_sizes, output_file, format, repo): """Render the dependency graph using Graphviz.""" # Fetch GitHub labels and colors label_colors = fetch_github_labels(repo) # eprint("Label colors:", label_colors) - dot = graphviz.Digraph(engine="sfdp", format=format) - dot.attr(splines="false", overlap="prism10000", bgcolor="#FFFFFF00", K="0.3", repulsiveforce="0.3") #sfdp + dot = graphviz.Digraph(engine='sfdp', format=format) + dot.attr(splines='false', overlap='prism10000', + bgcolor='#FFFFFF00', K='0.3', repulsiveforce='0.3') # sfdp max_lines = max(file_sizes.values(), default=1) - eprint("Maximum lines of code:", max_lines) - node_sizes = {node: max(0.05, 0.3 * math.sqrt(file_sizes.get(node, 0) / max_lines)) for node in graph} - node_colors = {node: module_based_color(node[:node.rfind(".")], label_colors) for node in graph} + eprint('Maximum lines of code:', max_lines) + node_sizes = {node: max( + 0.05, 0.3 * math.sqrt(file_sizes.get(node, 0) / max_lines)) for node in graph} + node_colors = {node: module_based_color( + node[:node.rfind('.')], label_colors) for node in graph} used_labels = set() label_counts = defaultdict(int) for node, dependencies in graph.items(): node_color = node_colors[node] - label = node[:node.rfind(".")] + label = node[:node.rfind('.')] used_labels.add(label) label_counts[label] += 1 - dot.node(node, shape="circle", style="filled", fillcolor=node_color, color="#FFFFFF00", width=str(node_sizes[node]), height=str(node_sizes[node]), label="") + dot.node(node, shape='circle', style='filled', fillcolor=node_color, color='#FFFFFF00', + width=str(node_sizes[node]), height=str(node_sizes[node]), label='') for dep in dependencies: if dep in graph: # Ensure we're not linking to removed nodes - edge_color = node_color + "10" - dot.edge(node, dep, color=edge_color, arrowhead="none") + edge_color = node_color + '10' + dot.edge(node, dep, color=edge_color, arrowhead='none') # Generate HTML legend - html_legend_output_file = output_file + "_legend.html" - generate_html_legend(label_colors, used_labels, html_legend_output_file, label_counts) - eprint(f"HTML Legend saved as {html_legend_output_file}") + html_legend_output_file = output_file + '_legend.html' + generate_html_legend(label_colors, used_labels, + html_legend_output_file, label_counts) + eprint(f'HTML Legend saved as {html_legend_output_file}') dot.render(output_file, format=format, cleanup=True) -if __name__ == "__main__": - root_dir = "src" + +if __name__ == '__main__': + root_dir = 'src' most_imported_drop_count = 20 - parser = argparse.ArgumentParser(description="Generate Agda dependency graph.") - parser.add_argument("output_file", type=str, help="Path to save the output graph.") - parser.add_argument("format", type=str, choices=["svg", "png", "pdf"], help="Output format of the graph.") + parser = argparse.ArgumentParser( + description='Generate Agda dependency graph.') + parser.add_argument('output_file', type=str, + help='Path to save the output graph.') + parser.add_argument('format', type=str, choices=[ + 'svg', 'png', 'pdf'], help='Output format of the graph.') args = parser.parse_args() - graph, file_sizes = build_dependency_graph(root_dir, most_imported_drop_count=most_imported_drop_count) - render_graph(graph, file_sizes, args.output_file, format=args.format, repo=GITHUB_REPO) - eprint(f"Graph saved as {args.output_file}.{args.format}") + graph, file_sizes = build_dependency_graph( + root_dir, most_imported_drop_count=most_imported_drop_count) + render_graph(graph, file_sizes, args.output_file, + format=args.format, repo=GITHUB_REPO) + eprint(f'Graph saved as {args.output_file}.{args.format}') diff --git a/scripts/generate_maintainers.py b/scripts/generate_maintainers.py index 86199ac49a8..c6f5351a390 100644 --- a/scripts/generate_maintainers.py +++ b/scripts/generate_maintainers.py @@ -33,8 +33,10 @@ def format_maintainer(maintainer): if __name__ == '__main__': parser = argparse.ArgumentParser( description='Generate maintainers markdown content. Usage: generate_maintainers.py ') - parser.add_argument('contributors_file', help='Path to the CONTRIBUTORS.toml file.') - parser.add_argument('output_file', help='Output file path to write the generated maintainers markdown content to.') + parser.add_argument('contributors_file', + help='Path to the CONTRIBUTORS.toml file.') + parser.add_argument( + 'output_file', help='Output file path to write the generated maintainers markdown content to.') args = parser.parse_args() contributors_data = parse_contributors_file(args.contributors_file) @@ -49,7 +51,8 @@ def format_maintainer(maintainer): out_path = args.output_file if os.path.isdir(out_path): - print(f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr) + print( + f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr) sys.exit(2) parent = os.path.dirname(out_path) if parent: diff --git a/scripts/generate_mdbook_summary.py b/scripts/generate_mdbook_summary.py index e220714f50c..c45aab2ec4f 100755 --- a/scripts/generate_mdbook_summary.py +++ b/scripts/generate_mdbook_summary.py @@ -33,11 +33,13 @@ def generate_namespace_entry_list(root_path, namespace): relevant_files = tuple( f for f in git_tracked_files if namespace_path in f.parents) - lagda_file_paths = tuple(f for f in relevant_files if utils.is_agda_file(f)) + lagda_file_paths = tuple( + f for f in relevant_files if utils.is_agda_file(f)) modules = tuple(p.name for p in lagda_file_paths) module_titles = tuple(utils.get_lagda_md_file_title(f) - for f in lagda_file_paths) - module_mdfiles = tuple(utils.get_module_mdfile(namespace, m) for m in modules) + for f in lagda_file_paths) + module_mdfiles = tuple(utils.get_module_mdfile(namespace, m) + for m in modules) # Check for missing titles for title, module in zip(module_titles, modules): @@ -65,7 +67,8 @@ def generate_namespace_entry_list(root_path, namespace): entry_list = (' ' + entry_template.format(title=t, mdfile=md) for t, md in module_titles_and_mdfiles) - namespace_title = utils.get_lagda_md_file_title(str(namespace_path.with_suffix('.lagda.md'))) + namespace_title = utils.get_lagda_md_file_title( + str(namespace_path.with_suffix('.lagda.md'))) namespace_entry = entry_template.format( title=namespace_title, mdfile=namespace + '.md') @@ -85,7 +88,8 @@ def generate_index(root_path): entry_lists.append(entry_list) status |= s - literature_index, lit_status = generate_namespace_entry_list(root_path, LITERATURE_MODULE) + literature_index, lit_status = generate_namespace_entry_list( + root_path, LITERATURE_MODULE) status |= lit_status index = '\n\n'.join(entry_lists) + '\n' @@ -133,8 +137,10 @@ def generate_index(root_path): parser = argparse.ArgumentParser( description='Generate mdbook SUMMARY file. Usage: generate_mdbook_summary.py ') - parser.add_argument('output_file', help='Output file path to write the generated SUMMARY markdown content to.') - parser.add_argument('--root', help='Root path to source.', default='src', required=False) + parser.add_argument( + 'output_file', help='Output file path to write the generated SUMMARY markdown content to.') + parser.add_argument('--root', help='Root path to source.', + default='src', required=False) args = parser.parse_args() @@ -157,12 +163,14 @@ def generate_index(root_path): print(f'No changes to {summary_file_path}.') else: summary_file_path.write_text(summary_contents) - print(f'Updated mdbook summary content at {summary_file_path}.') + print( + f'Updated mdbook summary content at {summary_file_path}.') else: summary_file_path.parent.mkdir(parents=True, exist_ok=True) summary_file_path.write_text(summary_contents) print(f'Wrote mdbook summary content to {summary_file_path}.') except Exception as e: - utils.eprint(f'Failed to write summary file {summary_file_path}: {e}') + utils.eprint( + f'Failed to write summary file {summary_file_path}: {e}') status |= STATUS_FAILED_OVERWRITE sys.exit(status) diff --git a/scripts/generate_noagda_html.py b/scripts/generate_noagda_html.py index 8a03999c104..9dc4ccc195e 100644 --- a/scripts/generate_noagda_html.py +++ b/scripts/generate_noagda_html.py @@ -22,7 +22,7 @@ sys.exit(STATUS_FLAG_GIT_ERROR) try: - outDir.mkdir(parents=True, exist_ok=True) + outDir.mkdir(parents=True, exist_ok=True) except FileExistsError: utils.eprint('Output path exists and is not a directory') sys.exit(STATUS_OUT_NOT_DIR) @@ -31,7 +31,7 @@ if fpath.parts[0] != root or not utils.is_agda_file(fpath): continue module_name = utils.get_agda_module_name(str(fpath), root) - dest = outDir / (module_name + ".md") + dest = outDir / (module_name + '.md') # Ideally we would try symlinks, but linkcheck always follows them and # then complains about links outside of the root directory diff --git a/scripts/markdown_conventions.py b/scripts/markdown_conventions.py index 1dd2b595769..d0edbc1f2d5 100755 --- a/scripts/markdown_conventions.py +++ b/scripts/markdown_conventions.py @@ -82,6 +82,7 @@ def check_unclosed_inline_code_guard(lines): return problematic_lines + def find_invalid_headings(lines): """ Finds headings which contain links. @@ -98,6 +99,7 @@ def find_invalid_headings(lines): return invalid_heading_lines + if __name__ == '__main__': STATUS_UNSPECIFIED_OR_ILL_FORMED_BLOCK = 1 @@ -121,7 +123,8 @@ def find_invalid_headings(lines): output = inputText lines = output.split('\n') - offender_line_number, offender_is_closing = find_ill_formed_block(lines) + offender_line_number, offender_is_closing = find_ill_formed_block( + lines) if offender_line_number is not None: if offender_is_closing: @@ -136,7 +139,7 @@ def find_invalid_headings(lines): # Check for unmatched backticks outside of Agda code blocks backtick_lines = check_unclosed_inline_code_guard(lines) if backtick_lines: - line_list = ", ".join(str(line) for line in backtick_lines) + line_list = ', '.join(str(line) for line in backtick_lines) print( f"Error! File '{fpath}' line(s) {line_list} contain backticks (`) for guarding inline code blocks that don't have matching closing or opening guards. Please add the matching backtick(s).") status |= STATUS_UNCLOSED_BACKTICK @@ -167,7 +170,7 @@ def find_invalid_headings(lines): status |= STATUS_INVALID_HEADING for line in invalid_heading_lines: print( - f"{line}:\t{lines[line-1]}") + f'{line}:\t{lines[line-1]}') # Remove empty code blocks output = empty_block_pattern.sub('', output) diff --git a/scripts/preprocessor_citations.py b/scripts/preprocessor_citations.py index 4b40cc1de53..2971c365b8b 100644 --- a/scripts/preprocessor_citations.py +++ b/scripts/preprocessor_citations.py @@ -47,7 +47,8 @@ def write_epilogue(self): self.output('\n\n') def write_entry(self, key, label, text): - self.output(f'
[{label}]
\n') + self.output( + f'
[{label}]
\n') self.output(f'
{text}
\n') @@ -106,7 +107,8 @@ def format_citation( return f'[{formatted_label}]' else: - eprint(f"Error! Citation key '{cite_key}' used in #cite macro was not found in bibliography. File: '{chapter['path']}'") + eprint( + f"Error! Citation key '{cite_key}' used in #cite macro was not found in bibliography. File: '{chapter['path']}'") unmatched_cite_keys.add(cite_key) # If the cite_key is not recognized, we make the following guess about how to format the citation instead of failing completely return f'[{cite_key}]' @@ -139,7 +141,8 @@ def sub_reference_regex_lambda(m): cited_keys.add(cite_key) return '' else: - eprint(f"Error! Citation key '{cite_key}' used in #reference macro was not found in bibliography. File: '{chapter['path']}'") + eprint( + f"Error! Citation key '{cite_key}' used in #reference macro was not found in bibliography. File: '{chapter['path']}'") unmatched_cite_keys.add(cite_key) return '' @@ -153,7 +156,8 @@ def sub_reference_regex_lambda(m): new_content, bibliography_section) elif BIBLIOGRAPHY_REGEX.search(new_content): - eprint(f"Error! A #bibliography macro was found, but there are no references. File: '{chapter['path']}'.") + eprint( + f"Error! A #bibliography macro was found, but there are no references. File: '{chapter['path']}'.") empty_bibliography_invocations.add(chapter['path']) chapter['content'] = new_content @@ -173,7 +177,7 @@ def insert_bibliography_at_correct_location(content, bibliography_section): lambda _: bibliography_section, content) else: # If the placeholder isn't found, append the bibliography at the end of the content, with a `## References` header - new_content = content + "\n\n## References\n\n" + bibliography_section + new_content = content + '\n\n## References\n\n' + bibliography_section return new_content @@ -210,7 +214,7 @@ def process_citations_root_section( def does_support_backend(backend): - return backend == 'html' or backend == "linkcheck" + return backend == 'html' or backend == 'linkcheck' if __name__ == '__main__': @@ -268,13 +272,15 @@ def does_support_backend(backend): json.dump(book, sys.stdout) if unmatched_cite_keys: - eprint("The following unmatched bibliography keys were found while processing citations: ", ", ".join(sorted(unmatched_cite_keys))) + eprint('The following unmatched bibliography keys were found while processing citations: ', + ', '.join(sorted(unmatched_cite_keys))) if citations_config.get('error-on-unmatched-keys', DEFAULT_ERROR_ON_UNMATCHED_CITE_KEY): sys.exit(1) if empty_bibliography_invocations: - eprint("The following files have #bibliography macro invocations with empty bibliographies: ", ", ".join(sorted(empty_bibliography_invocations))) + eprint('The following files have #bibliography macro invocations with empty bibliographies: ', + ', '.join(sorted(empty_bibliography_invocations))) if citations_config.get('error-on-empty-bibliography', DEFAULT_ERROR_ON_EMPTY_BIBLIOGRAPHY): sys.exit(2) diff --git a/scripts/preprocessor_git_metadata.py b/scripts/preprocessor_git_metadata.py index 5801441eafb..b7b0034e233 100644 --- a/scripts/preprocessor_git_metadata.py +++ b/scripts/preprocessor_git_metadata.py @@ -85,14 +85,15 @@ def get_author_element_for_file(filename, include_contributors, contributors, co # If all commits to a file are chore commits, then there are no authors if raw_authors_git_output: - # Collect authors and sort by number of commits - sorted_authors, __skipped_authors = sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors) - skipped_authors.update(__skipped_authors) - author_names = [ - author['displayName'] - for author in sorted_authors - ] - attribution_text = f'

Content created by {format_multiple_authors_attribution(author_names)}.

' + # Collect authors and sort by number of commits + sorted_authors, __skipped_authors = sorted_authors_from_raw_shortlog_lines( + raw_authors_git_output, contributors) + skipped_authors.update(__skipped_authors) + author_names = [ + author['displayName'] + for author in sorted_authors + ] + attribution_text = f'

Content created by {format_multiple_authors_attribution(author_names)}.

' file_log_output = subprocess.run([ 'git', 'log', @@ -225,10 +226,11 @@ def add_author_info_to_root_section(roots, section, contributors, config): metadata_config['suppress_processing'] = metadata_config.get( 'suppress_processing', []) metadata_config['contributors_file'] = metadata_config.get( - 'contributors_file', "CONTRIBUTORS.toml") + 'contributors_file', 'CONTRIBUTORS.toml') # Load the contributors data - contributors_data = parse_contributors_file(metadata_config['contributors_file']) + contributors_data = parse_contributors_file( + metadata_config['contributors_file']) if bool(metadata_config.get('enable')): # Split the work between PROCESS_COUNT processes diff --git a/scripts/remove_unused_imports.py b/scripts/remove_unused_imports.py index c1c56aaa4c9..8948cd4b59a 100755 --- a/scripts/remove_unused_imports.py +++ b/scripts/remove_unused_imports.py @@ -96,10 +96,12 @@ def get_agda_files(path): if os.path.isfile(path): return [path] if utils.is_agda_file(pathlib.Path(path)) else [] elif os.path.isdir(path): - def filter_agda_files(f): return utils.is_agda_file(pathlib.Path(f)) and os.path.dirname(f) != path + def filter_agda_files(f): return utils.is_agda_file( + pathlib.Path(f)) and os.path.dirname(f) != path return list(filter(filter_agda_files, utils.get_files_recursive(path))) else: - utils.multithread.thread_safe_print(f"Warning: '{path}' is not a valid file or directory. Skipping.") + utils.multithread.thread_safe_print( + f"Warning: '{path}' is not a valid file or directory. Skipping.") return [] @@ -126,7 +128,8 @@ def filter_agda_files(f): return utils.is_agda_file(pathlib.Path(f)) and os.path agda_files.extend(get_agda_files(path)) if not agda_files: - utils.multithread.thread_safe_print("No Agda files found in the specified paths.") + utils.multithread.thread_safe_print( + 'No Agda files found in the specified paths.') sys.exit(1) # Sort the files by Git modification status and last commit date diff --git a/scripts/requirements.txt b/scripts/requirements.txt index 851e3dd04e5..5afbdd09bc5 100644 --- a/scripts/requirements.txt +++ b/scripts/requirements.txt @@ -1,6 +1,5 @@ # * Keep in sync with the `flake.nix` file +graphviz pre-commit pybtex -requests tomli -graphviz diff --git a/scripts/typechecking_profile_parser.py b/scripts/typechecking_profile_parser.py index 6291b9ca8ba..88ca0cf2fc1 100644 --- a/scripts/typechecking_profile_parser.py +++ b/scripts/typechecking_profile_parser.py @@ -9,11 +9,11 @@ def parse_memory_profiling_data(filepath): # Define patterns to match each line and their corresponding unit patterns = { - "memory_allocated_in_heap": (r"(\d+(?:,\d+)*) bytes allocated in the heap", "B"), - "memory_copied_during_GC": (r"(\d+(?:,\d+)*) bytes copied during GC", "B"), - "maximum_residency": (r"(\d+(?:,\d+)*) bytes maximum residency", "B"), - "memory_maximum_slop": (r"(\d+(?:,\d+)*) bytes maximum slop", "B"), - "total_memory_in_use": (r"(\d+) MiB total memory in use", "MiB") + 'memory_allocated_in_heap': (r'(\d+(?:,\d+)*) bytes allocated in the heap', 'B'), + 'memory_copied_during_GC': (r'(\d+(?:,\d+)*) bytes copied during GC', 'B'), + 'maximum_residency': (r'(\d+(?:,\d+)*) bytes maximum residency', 'B'), + 'memory_maximum_slop': (r'(\d+(?:,\d+)*) bytes maximum slop', 'B'), + 'total_memory_in_use': (r'(\d+) MiB total memory in use', 'MiB') } with open(filepath, 'r') as file: @@ -21,17 +21,18 @@ def parse_memory_profiling_data(filepath): for key, (pattern, unit) in patterns.items(): match = re.search(pattern, line) if match: - value = int(match.group(1).replace(",", "")) - if key == "memory_maximum_slop": # Convert maximum slo to KiB and truncate + value = int(match.group(1).replace(',', '')) + if key == 'memory_maximum_slop': # Convert maximum slo to KiB and truncate value //= 1024 - unit = "KiB" - elif unit == "B": # Convert bytes to MiB and truncate + unit = 'KiB' + elif unit == 'B': # Convert bytes to MiB and truncate value //= 1024 * 1024 - unit = "MiB" - results[key] = {"value": value, "unit": unit} + unit = 'MiB' + results[key] = {'value': value, 'unit': unit} return results + def parse_benchmark_results(input_path): benchmarks = dict() with open(input_path, 'r') as file: @@ -41,8 +42,8 @@ def parse_benchmark_results(input_path): if match: name = match.group(1).strip() # Correctly parse and combine the number groups to handle commas in numbers - milliseconds = int(match.group(2).replace(',','')) - benchmarks[name] = {'value': milliseconds, 'unit':'ms'} + milliseconds = int(match.group(2).replace(',', '')) + benchmarks[name] = {'value': milliseconds, 'unit': 'ms'} return benchmarks @@ -52,12 +53,16 @@ def subdict(original_dict, keys_to_extract): else: return {key: original_dict[key] for key in keys_to_extract if key in original_dict} + def convert_dict_to_list(data, keys_to_extract=None): return [{'name': name, **details} for name, details in subdict(data, keys_to_extract).items()] + def save_github_action_benchmark_json(output_path, benchmarks, memory_stats, benchmark_keys, memory_keys): with open(output_path, 'w') as file: - json.dump(convert_dict_to_list(benchmarks, benchmark_keys) + convert_dict_to_list(memory_stats, memory_keys) , file, indent=2) + json.dump(convert_dict_to_list(benchmarks, benchmark_keys) + + convert_dict_to_list(memory_stats, memory_keys), file, indent=2) + def read_existing_csv_to_dict(csv_path, commit_hash): # Initialize a dictionary to hold the CSV data @@ -69,7 +74,8 @@ def read_existing_csv_to_dict(csv_path, commit_hash): with open(csv_path, mode='r', newline='') as csvfile: reader = csv.DictReader(csvfile) # Update fieldnames with those found in the existing CSV, plus the new commit hash if necessary - fieldnames = reader.fieldnames + [commit_hash] if commit_hash not in reader.fieldnames else reader.fieldnames + fieldnames = reader.fieldnames + \ + [commit_hash] if commit_hash not in reader.fieldnames else reader.fieldnames for row in reader: data_dict[row['name']] = row except FileNotFoundError: @@ -78,6 +84,7 @@ def read_existing_csv_to_dict(csv_path, commit_hash): return data_dict, fieldnames + def update_csv_data(data_dict, benchmarks, memory_stats, commit_hash): # Combine benchmarks and memory stats for easier processing combined_data = {**memory_stats, **benchmarks} @@ -88,19 +95,18 @@ def update_csv_data(data_dict, benchmarks, memory_stats, commit_hash): data_dict[name] = {'name': name, 'unit': details['unit']} data_dict[name][commit_hash] = int(details['value']) + def write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash): def custom_sort(item): # Sort all items that do not have unit "ms" first, then sort based on whether the name is capitalized, and then based on worst newest benchmark - is_not_ms_unit = item['unit'] != "ms" + is_not_ms_unit = item['unit'] != 'ms' if is_not_ms_unit: # If the unit is not `ms`, preserve order return (False, False, 0) else: # If the unit is `ms`, sort based on capitalization, then on newest benchmark - return (True , item['name'][0].islower(), 0 if commit_hash not in item.keys() else -item[commit_hash]) - - + return (True, item['name'][0].islower(), 0 if commit_hash not in item.keys() else -item[commit_hash]) with open(csv_path, mode='w', newline='') as csvfile: writer = csv.DictWriter(csvfile, fieldnames=fieldnames) @@ -110,17 +116,23 @@ def custom_sort(item): for row in sorted_data: writer.writerow(row) + def save_as_csv(benchmarks, memory_stats, csv_path, commit_hash): data_dict, fieldnames = read_existing_csv_to_dict(csv_path, commit_hash) update_csv_data(data_dict, benchmarks, memory_stats, commit_hash) write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash) -if __name__ == "__main__": + +if __name__ == '__main__': # Set up argument parsing - parser = argparse.ArgumentParser(description='Convert benchmark results to JSON format.') - parser.add_argument('input_times_path', help='Path to the input file containing typechecking times.') - parser.add_argument('input_memory_path', help='Path to the input file containing memory statistics.') - parser.add_argument('output_json_path', help='Path to the output JSON file.') + parser = argparse.ArgumentParser( + description='Convert benchmark results to JSON format.') + parser.add_argument( + 'input_times_path', help='Path to the input file containing typechecking times.') + parser.add_argument( + 'input_memory_path', help='Path to the input file containing memory statistics.') + parser.add_argument('output_json_path', + help='Path to the output JSON file.') parser.add_argument('csv_path', help='Path to the profiling CSV file.') parser.add_argument('commit_hash', help='Commit hash for current commit.') @@ -131,5 +143,6 @@ def save_as_csv(benchmarks, memory_stats, csv_path, commit_hash): benchmarks = parse_benchmark_results(args.input_times_path) memory_stats = parse_memory_profiling_data(args.input_memory_path) - save_github_action_benchmark_json(args.output_json_path, benchmarks, memory_stats, ["Total",], ["total_memory_in_use",]) + save_github_action_benchmark_json(args.output_json_path, benchmarks, memory_stats, [ + 'Total',], ['total_memory_in_use',]) save_as_csv(benchmarks, memory_stats, args.csv_path, args.commit_hash) diff --git a/scripts/utils/__init__.py b/scripts/utils/__init__.py index 02576ad898d..e2e0a86492d 100644 --- a/scripts/utils/__init__.py +++ b/scripts/utils/__init__.py @@ -221,6 +221,7 @@ def get_git_tracked_files(): git_tracked_files = map(pathlib.Path, git_output.strip().split('\0')[:-1]) return git_tracked_files + def get_git_last_modified(file_path): try: # Get the last commit date for the file @@ -238,9 +239,11 @@ def get_git_last_modified(file_path): # If the git command fails, fall back to filesystem modification time return os.path.getmtime(file_path) + def is_file_modified(file_path): try: - subprocess.check_output(['git', 'diff', '--quiet', file_path], stderr=subprocess.DEVNULL) + subprocess.check_output( + ['git', 'diff', '--quiet', file_path], stderr=subprocess.DEVNULL) return False except subprocess.CalledProcessError: return True @@ -249,17 +252,18 @@ def is_file_modified(file_path): def parse_agda_imports(agda_file: str) -> Set[str]: """Extract import statements from an Agda file.""" imports = set() - with open(agda_file, "r", encoding="utf-8") as f: + with open(agda_file, 'r', encoding='utf-8') as f: for line in f: - match = re.match(r"^\s*open\s+import\s+([A-Za-z0-9\-.]+)", line) + match = re.match(r'^\s*open\s+import\s+([A-Za-z0-9\-.]+)', line) if match: imports.add(match.group(1)) return imports + def count_lines_in_file(file_path: str) -> int: """Count lines of code in a file.""" try: - with open(file_path, "r", encoding="utf-8") as f: + with open(file_path, 'r', encoding='utf-8') as f: return sum(1 for _ in f) except Exception: return 0 diff --git a/scripts/utils/contributors.py b/scripts/utils/contributors.py index 3a7089125ac..adc33da8587 100644 --- a/scripts/utils/contributors.py +++ b/scripts/utils/contributors.py @@ -17,10 +17,12 @@ def print_skipping_contributor_warning(contributor, contributors_file): print(f'Warning: not attributing changes to {contributor}. If you want your work to be attributed to you, add yourself to {contributors_file}.', file=sys.stderr) + def print_skipping_contributors_warning(contributors, contributors_file): for contributor in sorted(contributors): print_skipping_contributor_warning(contributor, contributors_file) + def get_real_author_index(raw_username, contributors): return next((index for (index, c) in enumerate(contributors) if raw_username in c['usernames']), None) @@ -40,4 +42,4 @@ def sorted_authors_from_raw_shortlog_lines(shortlog, contributors): # print_skipping_contributor_warning(raw_author, contributors_file) sorted_author_indices = sorted( author_commits, key=author_commits.get, reverse=True) - return [contributors[author_index] for author_index in sorted_author_indices] , skipped_authors + return [contributors[author_index] for author_index in sorted_author_indices], skipped_authors diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md index 5aeafc52d49..074e9c4c78d 100644 --- a/src/foundation-core/propositions.lagda.md +++ b/src/foundation-core/propositions.lagda.md @@ -417,7 +417,7 @@ $n$-[types](foundation-core.truncated-types.md). | [Dependent sum](foundation.dependent-pair-types.md) | `Σ` | `Σ-Prop` | | [Dependent product](foundation.dependent-function-types.md) | `Π` | `Π-Prop` | | [Functions](foundation-core.function-types.md) | `→` | `⇒` | -| [Logical equivalence](foundation.logical-equivalences.md) | `↔` | `⇔` | +| [Logical equivalence](foundation.logical-equivalences.md) | `↔` | `⇔` | | [Product](foundation-core.cartesian-product-types.md) | `×` | `product-Prop` | | [Join](synthetic-homotopy-theory.joins-of-types.md) | `*` | `join-Prop` | | [Exclusive sum](foundation.exclusive-sum.md) | `exclusive-sum` | `exclusive-sum-Prop` | diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index ef3bcc5babf..bdbace6785d 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -49,8 +49,8 @@ open import foundation-core.type-theoretic-principle-of-choice ### Any equivalence is an embedding We already proved in `foundation-core.equivalences` that equivalences are -embeddings. Here we have `_↪_` available, so we record the map from equivalences -to embeddings. +embeddings. Here we have `_↪_` available, so we record the map from +equivalences to embeddings. ```agda module _ diff --git a/src/foundation/propositions.lagda.md b/src/foundation/propositions.lagda.md index e4bf1eb7730..2f87c4f4b8c 100644 --- a/src/foundation/propositions.lagda.md +++ b/src/foundation/propositions.lagda.md @@ -116,7 +116,7 @@ $n$-[types](foundation-core.truncated-types.md). | [Dependent sum](foundation.dependent-pair-types.md) | `Σ` | `Σ-Prop` | | [Dependent product](foundation.dependent-function-types.md) | `Π` | `Π-Prop` | | [Functions](foundation-core.function-types.md) | `→` | `⇒` | -| [Logical equivalence](foundation.logical-equivalences.md) | `↔` | `⇔` | +| [Logical equivalence](foundation.logical-equivalences.md) | `↔` | `⇔` | | [Product](foundation-core.cartesian-product-types.md) | `×` | `product-Prop` | | [Join](synthetic-homotopy-theory.joins-of-types.md) | `*` | `join-Prop` | | [Exclusive sum](foundation.exclusive-sum.md) | `exclusive-sum` | `exclusive-sum-Prop` | diff --git a/website/theme/css/chrome.css b/website/theme/css/chrome.css index 63f4f749a52..84c8f503caf 100644 --- a/website/theme/css/chrome.css +++ b/website/theme/css/chrome.css @@ -158,13 +158,17 @@ a > .hljs { align-content: center; flex-direction: column; - transition: color 0.5s, background-color 0.5s; + transition: + color 0.5s, + background-color 0.5s; } .nav-chapters:hover { text-decoration: none; background-color: var(--theme-hover); - transition: background-color 0.15s, color 0.15s; + transition: + background-color 0.15s, + color 0.15s; } .nav-wrapper { @@ -240,7 +244,9 @@ pre > .buttons { cursor: pointer; visibility: hidden; opacity: 0; - transition: visibility 0.1s linear, opacity 0.1s linear; + transition: + visibility 0.1s linear, + opacity 0.1s linear; } pre:hover > .buttons { visibility: visible; diff --git a/website/theme/css/general.css b/website/theme/css/general.css index b6c7fc24153..55aa1551f8a 100644 --- a/website/theme/css/general.css +++ b/website/theme/css/general.css @@ -110,7 +110,9 @@ h6:target::before { box-sizing: border-box; } .js:not(.sidebar-resizing) .page-wrapper { - transition: margin-left 0.3s ease, transform 0.3s ease; /* Animation: slide away */ + transition: + margin-left 0.3s ease, + transform 0.3s ease; /* Animation: slide away */ } .content { @@ -161,11 +163,11 @@ a.concept { } :is( - nav.pagetoc a, - a:has(> img), - a.concept[href^='http'], - .hide-external-link - )::after { + nav.pagetoc a, + a:has(> img), + a.concept[href^='http'], + .hide-external-link +)::after { display: none !important; } .content img, diff --git a/website/theme/css/variables.css b/website/theme/css/variables.css index fe8e3393e3d..85a6e2a7cde 100644 --- a/website/theme/css/variables.css +++ b/website/theme/css/variables.css @@ -5,9 +5,9 @@ --page-padding: 5px; --content-max-width: 75%; --menu-bar-height: 40px; - --mono-font: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, - Liberation Mono, DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New, - monospace; + --mono-font: + Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, Liberation Mono, + DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New, monospace; --code-font-size: 1.3rem; --pagetoc-fontsize: 0.85em; }