Organize repository files

.editorconfig

@@ -31,3 +31,8 @@ indent_size = 4
 
 [*.{ya?ml,cff}]
 indent_size = 2
+
+[Makefile]
+indent_style = tab
+indent_size = 2
+trim_trailing_whitespace = false

.gitignore

@@ -420,15 +420,11 @@ node_modules/*
 package-lock.json
 
 # mdbook, automatically generated files
-docs/
 html/
 book/
 temp/
 src/temp/
 src/everything.lagda.md
-SUMMARY.md
-CONTRIBUTORS.md
-MAINTAINERS.md
 /website/css/Agda-highlight.css
 /website/images/agda_dependency_graph.svg
 /website/images/agda_dependency_graph_legend.html

.pre-commit-config.yaml

@@ -22,11 +22,11 @@ repos:
         args:
           [
             '--config',
-            '.codespellrc',
+            'config/codespellrc',
             '--builtin',
             'clear,rare,informal,usage,code,names,en-GB_to_en-US',
             '--dictionary',
-            'codespell-dictionary.txt,-',
+            'config/codespell-dictionary.txt,-',
           ]
 
   - repo: local
@@ -35,7 +35,7 @@ repos:
         name: Sort codespell dictionary and ignore files
         entry: bash -c 'for f in "$@"; do LC_ALL=C sort -o "$f" "$f"; done' --
         language: system
-        files: ^codespell-(dictionary|ignore)\.txt$
+        files: ^config/codespell-(dictionary|ignore)\.txt$
       - id: markdown-conventions
         name: Markdown conventions
         entry: scripts/markdown_conventions.py
@@ -96,21 +96,13 @@ repos:
         require_serial: true
 
       - id: generate-namespace-index-modules
-        name: Generate Agda namespace index modules
+        name: Generate namespace indexes of modules
         entry: scripts/generate_namespace_index_modules.py
         language: python
         always_run: true
         pass_filenames: false
         require_serial: true
 
-      - id: generate-main-index-file
-        name: Generate main index file
-        entry: scripts/generate_main_index_file.py
-        language: python
-        always_run: true
-        pass_filenames: false
-        require_serial: true
-
       # ! Experimental hook
       # - id: spaces-convention
       #   name: Check Agda code block spaces convention
@@ -141,6 +133,7 @@ repos:
       - id: prettier
         name: CSS, JS, YAML and Markdown (no codeblocks) formatting
         types_or: [css, javascript, yaml, markdown]
+        args: ['--config', '.prettierrc.json']
 
   - repo: https://github.com/FlamingTempura/bibtex-tidy
     rev: v1.14.0

.vscode/settings.json

@@ -94,7 +94,8 @@
 
   "[makefile]": {
     "editor.insertSpaces": false,
-    "editor.detectIndentation": true
+    "editor.detectIndentation": false,
+    "editor.renderWhitespace": "boundary"
   },
 
   "[markdown]": {

CONTRIBUTING.md

@@ -43,11 +43,11 @@ Below is a summary of the tasks this tool performs:
   permissible spellchecker that only reports known misspellings, rather than
   words it does not recognize. I.e., it is a blacklist based spellchecker. We
   maintain an additional library-defined dictionary of misspellings at:
-  [`codespell-dictionary.txt`](https://github.com/UniMath/agda-unimath/blob/master/codespell-dictionary.txt).
+  [`config/codespell-dictionary.txt`](https://github.com/UniMath/agda-unimath/blob/master/config/codespell-dictionary.txt).
   If you find a misspelled word in the library, it is good practice to add it to
   this dictionary in addition to correcting the mistake. If codespell
   erroneously reports a word as misspelled, please add it to
-  [`codespell-ignore.txt`](https://github.com/UniMath/agda-unimath/blob/master/codespell-ignore.txt).
+  [`config/codespell-ignore.txt`](https://github.com/UniMath/agda-unimath/blob/master/config/codespell-ignore.txt).
 
 - **Sort codespell dictionary and ignore files**: Sorts and formats the
   associated codespell dictionary and ignore files.
@@ -87,15 +87,11 @@ Below is a summary of the tasks this tool performs:
   and reports them. Note that single tokens such as long names can exceed this
   limit.
 
-- **Create index of modules**: Generates and maintains the index of modules for
-  each folder in `src`. For example, the `group-theory/` folder has a
-  corresponding `src/group-theory.lagda.md` file that imports all the modules in
-  `group-theory/` publicly. You do not need to maintain these files manually.
-
-- **Generate index file for the entire library**: Generates
-  `src/everything.lagda.md`, which imports all formalization files across the
-  library. This file is also regenerated by `make check` each time it's run. No
-  manual maintenance is required for this file.
+- **Generate namespace indexes of modules**: Generates and maintains the indexes
+  of modules for each folder in `src`. For example, the `group-theory/` folder
+  has a corresponding `src/group-theory.lagda.md` file that imports all the
+  modules in `group-theory/` publicly. You do not need to maintain these files
+  manually, although they can be edited.
 
 **Note**: The previous two hooks only detect tracked files. This means that if
 you add or delete files, they must be staged for these hooks to take these