From 947e300dd91e0de70929643fc1ce93af01a35a8e Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Sun, 5 Nov 2023 01:17:12 +0000 Subject: [PATCH] [ fix #1743 ] move README to `doc/` directory (#2184) * [ admin ] dev playground * [ fix #1743 ] move README to doc/ directory * [ fix ] whitespace violations * [ ci ] update to cope with new doc/ directory * [ cleanup ] remove stale reference to travis.yml * [ admin ] update README-related instructions * [ admin ] fix build badges * [ fix ] `make test` build * Moved contents of notes/ to doc/ * Added CHANGELOG entry --------- Co-authored-by: MatthewDaggitt --- {travis => .github/tooling}/agda-logo.svg | 0 {travis => .github/tooling}/index.agda | 0 {travis => .github/tooling}/index.sh | 0 .../tooling}/landing-bottom.html | 0 {travis => .github/tooling}/landing-top.html | 0 {travis => .github/tooling}/landing.sh | 0 .github/workflows/ci-ubuntu.yml | 6 +-- CHANGELOG.md | 11 ++++++ GNUmakefile | 10 +++-- GenerateEverything.hs | 37 +++++++++++++++---- HACKING.md | 25 ++++--------- README.md | 4 +- dev/.gitignore | 1 + dev/README.md | 4 ++ dev/experimental.agda-lib | 4 ++ README.agda => doc/README.agda | 0 {README => doc/README}/Axiom.agda | 0 {README => doc/README}/Case.agda | 0 {README => doc/README}/Data.agda | 0 .../README}/Data/Container/FreeMonad.agda | 0 .../README}/Data/Container/Indexed.agda | 0 {README => doc/README}/Data/Default.agda | 0 .../README}/Data/Fin/Relation/Unary/Top.agda | 0 .../Data/Fin/Substitution/UntypedLambda.agda | 0 {README => doc/README}/Data/Integer.agda | 0 {README => doc/README}/Data/List.agda | 0 {README => doc/README}/Data/List/Fresh.agda | 0 .../README}/Data/List/Membership.agda | 0 .../Data/List/Relation/Binary/Equality.agda | 0 .../List/Relation/Binary/Permutation.agda | 0 .../Data/List/Relation/Binary/Pointwise.agda | 0 .../Data/List/Relation/Binary/Subset.agda | 0 .../List/Relation/Ternary/Interleaving.agda | 0 .../README}/Data/List/Relation/Unary/All.agda | 0 .../README}/Data/List/Relation/Unary/Any.agda | 0 {README => doc/README}/Data/Nat.agda | 0 .../README}/Data/Nat/Induction.agda | 0 {README => doc/README}/Data/Record.agda | 0 {README => doc/README}/Data/Tree/AVL.agda | 0 {README => doc/README}/Data/Tree/Binary.agda | 0 {README => doc/README}/Data/Tree/Rose.agda | 0 .../README}/Data/Trie/NonDependent.agda | 0 .../Vec/Relation/Binary/Equality/Cast.agda | 0 {README => doc/README}/Data/Wrap.agda | 0 {README => doc/README}/Debug/Trace.agda | 0 .../README}/Design/Decidability.agda | 0 {README => doc/README}/Design/Fixity.agda | 0 .../README}/Design/Hierarchies.agda | 0 {README => doc/README}/Foreign/Haskell.agda | 0 .../README}/Function/Reasoning.agda | 0 {README => doc/README}/IO.agda | 0 {README => doc/README}/Inspect.agda | 0 {README => doc/README}/Nary.agda | 0 .../README}/Reflection/External.agda | 0 .../README}/Relation/Binary/TypeClasses.agda | 0 {README => doc/README}/Tactic/Cong.agda | 0 .../README}/Tactic/MonoidSolver.agda | 0 {README => doc/README}/Tactic/RingSolver.agda | 0 {README => doc/README}/Text/Pretty.agda | 0 {README => doc/README}/Text/Printf.agda | 0 {README => doc/README}/Text/Regex.agda | 0 {README => doc/README}/Text/Tabular.agda | 0 {notes => doc}/installation-guide.md | 0 {notes => doc}/release-guide.txt | 12 +----- doc/standard-library-doc.agda-lib | 4 ++ {notes => doc}/style-guide.md | 0 {notes => doc}/updating-experimental.txt | 0 fix-whitespace.yaml | 1 - 68 files changed, 76 insertions(+), 43 deletions(-) rename {travis => .github/tooling}/agda-logo.svg (100%) rename {travis => .github/tooling}/index.agda (100%) rename {travis => .github/tooling}/index.sh (100%) rename {travis => .github/tooling}/landing-bottom.html (100%) rename {travis => .github/tooling}/landing-top.html (100%) rename {travis => .github/tooling}/landing.sh (100%) create mode 100644 dev/.gitignore create mode 100644 dev/README.md create mode 100644 dev/experimental.agda-lib rename README.agda => doc/README.agda (100%) rename {README => doc/README}/Axiom.agda (100%) rename {README => doc/README}/Case.agda (100%) rename {README => doc/README}/Data.agda (100%) rename {README => doc/README}/Data/Container/FreeMonad.agda (100%) rename {README => doc/README}/Data/Container/Indexed.agda (100%) rename {README => doc/README}/Data/Default.agda (100%) rename {README => doc/README}/Data/Fin/Relation/Unary/Top.agda (100%) rename {README => doc/README}/Data/Fin/Substitution/UntypedLambda.agda (100%) rename {README => doc/README}/Data/Integer.agda (100%) rename {README => doc/README}/Data/List.agda (100%) rename {README => doc/README}/Data/List/Fresh.agda (100%) rename {README => doc/README}/Data/List/Membership.agda (100%) rename {README => doc/README}/Data/List/Relation/Binary/Equality.agda (100%) rename {README => doc/README}/Data/List/Relation/Binary/Permutation.agda (100%) rename {README => doc/README}/Data/List/Relation/Binary/Pointwise.agda (100%) rename {README => doc/README}/Data/List/Relation/Binary/Subset.agda (100%) rename {README => doc/README}/Data/List/Relation/Ternary/Interleaving.agda (100%) rename {README => doc/README}/Data/List/Relation/Unary/All.agda (100%) rename {README => doc/README}/Data/List/Relation/Unary/Any.agda (100%) rename {README => doc/README}/Data/Nat.agda (100%) rename {README => doc/README}/Data/Nat/Induction.agda (100%) rename {README => doc/README}/Data/Record.agda (100%) rename {README => doc/README}/Data/Tree/AVL.agda (100%) rename {README => doc/README}/Data/Tree/Binary.agda (100%) rename {README => doc/README}/Data/Tree/Rose.agda (100%) rename {README => doc/README}/Data/Trie/NonDependent.agda (100%) rename {README => doc/README}/Data/Vec/Relation/Binary/Equality/Cast.agda (100%) rename {README => doc/README}/Data/Wrap.agda (100%) rename {README => doc/README}/Debug/Trace.agda (100%) rename {README => doc/README}/Design/Decidability.agda (100%) rename {README => doc/README}/Design/Fixity.agda (100%) rename {README => doc/README}/Design/Hierarchies.agda (100%) rename {README => doc/README}/Foreign/Haskell.agda (100%) rename {README => doc/README}/Function/Reasoning.agda (100%) rename {README => doc/README}/IO.agda (100%) rename {README => doc/README}/Inspect.agda (100%) rename {README => doc/README}/Nary.agda (100%) rename {README => doc/README}/Reflection/External.agda (100%) rename {README => doc/README}/Relation/Binary/TypeClasses.agda (100%) rename {README => doc/README}/Tactic/Cong.agda (100%) rename {README => doc/README}/Tactic/MonoidSolver.agda (100%) rename {README => doc/README}/Tactic/RingSolver.agda (100%) rename {README => doc/README}/Text/Pretty.agda (100%) rename {README => doc/README}/Text/Printf.agda (100%) rename {README => doc/README}/Text/Regex.agda (100%) rename {README => doc/README}/Text/Tabular.agda (100%) rename {notes => doc}/installation-guide.md (100%) rename {notes => doc}/release-guide.txt (85%) create mode 100644 doc/standard-library-doc.agda-lib rename {notes => doc}/style-guide.md (100%) rename {notes => doc}/updating-experimental.txt (100%) diff --git a/travis/agda-logo.svg b/.github/tooling/agda-logo.svg similarity index 100% rename from travis/agda-logo.svg rename to .github/tooling/agda-logo.svg diff --git a/travis/index.agda b/.github/tooling/index.agda similarity index 100% rename from travis/index.agda rename to .github/tooling/index.agda diff --git a/travis/index.sh b/.github/tooling/index.sh similarity index 100% rename from travis/index.sh rename to .github/tooling/index.sh diff --git a/travis/landing-bottom.html b/.github/tooling/landing-bottom.html similarity index 100% rename from travis/landing-bottom.html rename to .github/tooling/landing-bottom.html diff --git a/travis/landing-top.html b/.github/tooling/landing-top.html similarity index 100% rename from travis/landing-top.html rename to .github/tooling/landing-top.html diff --git a/travis/landing.sh b/.github/tooling/landing.sh similarity index 100% rename from travis/landing.sh rename to .github/tooling/landing.sh diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 51c5f7b09c..9ac08748df 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -51,7 +51,7 @@ env: CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' - AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/ + AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -isrc -idoc jobs: test-stdlib: @@ -152,7 +152,7 @@ jobs: - name: Test stdlib run: | cabal run GenerateEverything - cp travis/* . + cp .github/tooling/* . ./index.sh ${{ env.AGDA }} --safe EverythingSafe.agda ${{ env.AGDA }} index.agda @@ -178,7 +178,7 @@ jobs: rm -f '${{ env.AGDA_HTML_DIR }}'/*.css ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda - cp travis/* . + cp .github/tooling/* . ./landing.sh - name: Deploy HTML diff --git a/CHANGELOG.md b/CHANGELOG.md index 479eb395bc..562c089ddf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1196,6 +1196,17 @@ Other major improvements * We have then moved raw bundles defined in `Data.X.Properties` to `Data.X.Base` for `X` = `Nat`/`Nat.Binary`/`Integer`/`Rational`/`Rational.Unnormalised`. + +### Upgrades to `README` sub-library + +* The `README` sub-library has been moved to `doc/README` and a new `doc/standard-library-doc.agda-lib` has been added. + +* The first consequence is that `README` files now can be type-checked in Emacs + using an out-of-the-box standard Agda installation without altering the main + `standard-library.agda-lib` file. + +* The second is that the `README` files are now their own first-class library + and can be imported like an other library. Deprecated modules ------------------ diff --git a/GNUmakefile b/GNUmakefile index 685d1c990b..e744f066cc 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -9,11 +9,14 @@ AGDA=$(AGDA_EXEC) $(AGDA_OPTIONS) $(AGDA_RTS_OPTIONS) # cabal install fix-whitespace test: Everything.agda check-whitespace - $(AGDA) -i. -isrc README.agda + cd doc && $(AGDA) README.agda testsuite: $(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only) +fix-whitespace: + cabal exec -- fix-whitespace + check-whitespace: cabal exec -- fix-whitespace --check @@ -21,11 +24,12 @@ setup: Everything.agda .PHONY: Everything.agda Everything.agda: - cabal run GenerateEverything + cabal run GenerateEverything -- --out-dir doc .PHONY: listings listings: Everything.agda - $(AGDA) -i. -isrc --html README.agda -v0 + cd doc && $(AGDA) --html README.agda -v0 clean : find . -type f -name '*.agdai' -delete + rm -f Everything.agda EverythingSafe.agda diff --git a/GenerateEverything.hs b/GenerateEverything.hs index ee49679f3a..edea56a0f0 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -1,5 +1,6 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} import Control.Applicative import Control.Monad @@ -299,18 +300,37 @@ checkFilePaths cat fps = forM_ fps $ \ fp -> do unless b $ die $ fp ++ " is listed as " ++ cat ++ " but does not exist." +data Options = Options + { includeDeprecated :: Bool + , outputDirectory :: FilePath + } + +initOptions :: Options +initOptions = Options + { includeDeprecated = False + , outputDirectory = "." + } + +parseOptions :: [String] -> Options -> Maybe Options +parseOptions [] opts = pure opts +parseOptions ("--include-deprecated" : rest) opts + = parseOptions rest (opts { includeDeprecated = True }) +parseOptions ("--out-dir" : dir : rest) opts + = parseOptions rest (opts { outputDirectory = dir }) +parseOptions _ _ = Nothing + --------------------------------------------------------------------------- -- Collecting all non-Core library files, analysing them and generating --- 4 files: +-- 2 files: -- Everything.agda all the modules -- EverythingSafe.agda all the safe modules +main :: IO () main = do args <- getArgs - includeDeprecated <- case args of - [] -> return False - ["--include-deprecated"] -> return True - _ -> hPutStr stderr usage >> exitFailure + Options{..} <- case parseOptions args initOptions of + Just opts -> pure opts + Nothing -> hPutStr stderr usage >> exitFailure checkFilePaths "unsafe" unsafeModules checkFilePaths "using K" withKModules @@ -325,14 +345,14 @@ main = do let mkModule str = "module " ++ str ++ " where" - writeFileUTF8 (allOutputFile ++ ".agda") $ + writeFileUTF8 (outputDirectory ++ "/" ++ allOutputFile ++ ".agda") $ unlines [ header , "{-# OPTIONS --rewriting --guardedness --sized-types #-}\n" , mkModule allOutputFile , format libraryfiles ] - writeFileUTF8 (safeOutputFile ++ ".agda") $ + writeFileUTF8 (outputDirectory ++ "/" ++ safeOutputFile ++ ".agda") $ unlines [ header , "{-# OPTIONS --safe --guardedness #-}\n" , mkModule safeOutputFile @@ -353,6 +373,9 @@ usage = unlines , "The program generates documentation for the library by extracting" , "headers from library modules. The output is written to " ++ allOutputFile , "with the file " ++ headerFile ++ " inserted verbatim at the beginning." + , "" + , "If the option --out-dir is used then the output is placed in the" + , "subdirectory thus selected." ] diff --git a/HACKING.md b/HACKING.md index b2d619ec32..b7573188b5 100644 --- a/HACKING.md +++ b/HACKING.md @@ -244,23 +244,14 @@ you are never committing anything with a whitespace violation: Type-checking the README directory ---------------------------------- -* By default the README directory is not exported in the - `standard-library.agda-lib` file in order to avoid clashing with other people's - README files. This means that by default type-checking a file in the README - directory fails. - -* If you wish to type-check a README file, then you will need to change the line: - ``` - include: src - ``` - to - ``` - include: src . - ``` - in the `standard-library.agda-lib` file. - -* Please do not include this change in your pull request. - +* By default the README files are not exported in the + `standard-library.agda-lib` file in order to avoid + clashing with other people's README files. + +* If you wish to type-check a README file, then you will + need to change the present working directory to `doc/` + where an appropriate `standard-library-doc.agda-lib` + file is present. Continuous Integration (CI) =========================== diff --git a/README.md b/README.md index 16a2f10959..f9489e81f3 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -![Travis (.org) branch](https://img.shields.io/travis/agda/agda-stdlib/master?label=master) -![Travis (.org) branch](https://img.shields.io/travis/agda/agda-stdlib/experimental?label=experimental) +[![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml) +[![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg?branch=experimental)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml) The Agda standard library ========================= diff --git a/dev/.gitignore b/dev/.gitignore new file mode 100644 index 0000000000..f59ec20aab --- /dev/null +++ b/dev/.gitignore @@ -0,0 +1 @@ +* \ No newline at end of file diff --git a/dev/README.md b/dev/README.md new file mode 100644 index 0000000000..d97d344209 --- /dev/null +++ b/dev/README.md @@ -0,0 +1,4 @@ +# Development playground + +This directory allows you to develop modules against the current dev +version of the stdlib as it currently sits in `src/`. diff --git a/dev/experimental.agda-lib b/dev/experimental.agda-lib new file mode 100644 index 0000000000..cb094977d8 --- /dev/null +++ b/dev/experimental.agda-lib @@ -0,0 +1,4 @@ +name: standard-library-dev +include: . ../src +flags: + --warning=noUnsupportedIndexedMatch diff --git a/README.agda b/doc/README.agda similarity index 100% rename from README.agda rename to doc/README.agda diff --git a/README/Axiom.agda b/doc/README/Axiom.agda similarity index 100% rename from README/Axiom.agda rename to doc/README/Axiom.agda diff --git a/README/Case.agda b/doc/README/Case.agda similarity index 100% rename from README/Case.agda rename to doc/README/Case.agda diff --git a/README/Data.agda b/doc/README/Data.agda similarity index 100% rename from README/Data.agda rename to doc/README/Data.agda diff --git a/README/Data/Container/FreeMonad.agda b/doc/README/Data/Container/FreeMonad.agda similarity index 100% rename from README/Data/Container/FreeMonad.agda rename to doc/README/Data/Container/FreeMonad.agda diff --git a/README/Data/Container/Indexed.agda b/doc/README/Data/Container/Indexed.agda similarity index 100% rename from README/Data/Container/Indexed.agda rename to doc/README/Data/Container/Indexed.agda diff --git a/README/Data/Default.agda b/doc/README/Data/Default.agda similarity index 100% rename from README/Data/Default.agda rename to doc/README/Data/Default.agda diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/doc/README/Data/Fin/Relation/Unary/Top.agda similarity index 100% rename from README/Data/Fin/Relation/Unary/Top.agda rename to doc/README/Data/Fin/Relation/Unary/Top.agda diff --git a/README/Data/Fin/Substitution/UntypedLambda.agda b/doc/README/Data/Fin/Substitution/UntypedLambda.agda similarity index 100% rename from README/Data/Fin/Substitution/UntypedLambda.agda rename to doc/README/Data/Fin/Substitution/UntypedLambda.agda diff --git a/README/Data/Integer.agda b/doc/README/Data/Integer.agda similarity index 100% rename from README/Data/Integer.agda rename to doc/README/Data/Integer.agda diff --git a/README/Data/List.agda b/doc/README/Data/List.agda similarity index 100% rename from README/Data/List.agda rename to doc/README/Data/List.agda diff --git a/README/Data/List/Fresh.agda b/doc/README/Data/List/Fresh.agda similarity index 100% rename from README/Data/List/Fresh.agda rename to doc/README/Data/List/Fresh.agda diff --git a/README/Data/List/Membership.agda b/doc/README/Data/List/Membership.agda similarity index 100% rename from README/Data/List/Membership.agda rename to doc/README/Data/List/Membership.agda diff --git a/README/Data/List/Relation/Binary/Equality.agda b/doc/README/Data/List/Relation/Binary/Equality.agda similarity index 100% rename from README/Data/List/Relation/Binary/Equality.agda rename to doc/README/Data/List/Relation/Binary/Equality.agda diff --git a/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda similarity index 100% rename from README/Data/List/Relation/Binary/Permutation.agda rename to doc/README/Data/List/Relation/Binary/Permutation.agda diff --git a/README/Data/List/Relation/Binary/Pointwise.agda b/doc/README/Data/List/Relation/Binary/Pointwise.agda similarity index 100% rename from README/Data/List/Relation/Binary/Pointwise.agda rename to doc/README/Data/List/Relation/Binary/Pointwise.agda diff --git a/README/Data/List/Relation/Binary/Subset.agda b/doc/README/Data/List/Relation/Binary/Subset.agda similarity index 100% rename from README/Data/List/Relation/Binary/Subset.agda rename to doc/README/Data/List/Relation/Binary/Subset.agda diff --git a/README/Data/List/Relation/Ternary/Interleaving.agda b/doc/README/Data/List/Relation/Ternary/Interleaving.agda similarity index 100% rename from README/Data/List/Relation/Ternary/Interleaving.agda rename to doc/README/Data/List/Relation/Ternary/Interleaving.agda diff --git a/README/Data/List/Relation/Unary/All.agda b/doc/README/Data/List/Relation/Unary/All.agda similarity index 100% rename from README/Data/List/Relation/Unary/All.agda rename to doc/README/Data/List/Relation/Unary/All.agda diff --git a/README/Data/List/Relation/Unary/Any.agda b/doc/README/Data/List/Relation/Unary/Any.agda similarity index 100% rename from README/Data/List/Relation/Unary/Any.agda rename to doc/README/Data/List/Relation/Unary/Any.agda diff --git a/README/Data/Nat.agda b/doc/README/Data/Nat.agda similarity index 100% rename from README/Data/Nat.agda rename to doc/README/Data/Nat.agda diff --git a/README/Data/Nat/Induction.agda b/doc/README/Data/Nat/Induction.agda similarity index 100% rename from README/Data/Nat/Induction.agda rename to doc/README/Data/Nat/Induction.agda diff --git a/README/Data/Record.agda b/doc/README/Data/Record.agda similarity index 100% rename from README/Data/Record.agda rename to doc/README/Data/Record.agda diff --git a/README/Data/Tree/AVL.agda b/doc/README/Data/Tree/AVL.agda similarity index 100% rename from README/Data/Tree/AVL.agda rename to doc/README/Data/Tree/AVL.agda diff --git a/README/Data/Tree/Binary.agda b/doc/README/Data/Tree/Binary.agda similarity index 100% rename from README/Data/Tree/Binary.agda rename to doc/README/Data/Tree/Binary.agda diff --git a/README/Data/Tree/Rose.agda b/doc/README/Data/Tree/Rose.agda similarity index 100% rename from README/Data/Tree/Rose.agda rename to doc/README/Data/Tree/Rose.agda diff --git a/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda similarity index 100% rename from README/Data/Trie/NonDependent.agda rename to doc/README/Data/Trie/NonDependent.agda diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda similarity index 100% rename from README/Data/Vec/Relation/Binary/Equality/Cast.agda rename to doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda diff --git a/README/Data/Wrap.agda b/doc/README/Data/Wrap.agda similarity index 100% rename from README/Data/Wrap.agda rename to doc/README/Data/Wrap.agda diff --git a/README/Debug/Trace.agda b/doc/README/Debug/Trace.agda similarity index 100% rename from README/Debug/Trace.agda rename to doc/README/Debug/Trace.agda diff --git a/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda similarity index 100% rename from README/Design/Decidability.agda rename to doc/README/Design/Decidability.agda diff --git a/README/Design/Fixity.agda b/doc/README/Design/Fixity.agda similarity index 100% rename from README/Design/Fixity.agda rename to doc/README/Design/Fixity.agda diff --git a/README/Design/Hierarchies.agda b/doc/README/Design/Hierarchies.agda similarity index 100% rename from README/Design/Hierarchies.agda rename to doc/README/Design/Hierarchies.agda diff --git a/README/Foreign/Haskell.agda b/doc/README/Foreign/Haskell.agda similarity index 100% rename from README/Foreign/Haskell.agda rename to doc/README/Foreign/Haskell.agda diff --git a/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda similarity index 100% rename from README/Function/Reasoning.agda rename to doc/README/Function/Reasoning.agda diff --git a/README/IO.agda b/doc/README/IO.agda similarity index 100% rename from README/IO.agda rename to doc/README/IO.agda diff --git a/README/Inspect.agda b/doc/README/Inspect.agda similarity index 100% rename from README/Inspect.agda rename to doc/README/Inspect.agda diff --git a/README/Nary.agda b/doc/README/Nary.agda similarity index 100% rename from README/Nary.agda rename to doc/README/Nary.agda diff --git a/README/Reflection/External.agda b/doc/README/Reflection/External.agda similarity index 100% rename from README/Reflection/External.agda rename to doc/README/Reflection/External.agda diff --git a/README/Relation/Binary/TypeClasses.agda b/doc/README/Relation/Binary/TypeClasses.agda similarity index 100% rename from README/Relation/Binary/TypeClasses.agda rename to doc/README/Relation/Binary/TypeClasses.agda diff --git a/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda similarity index 100% rename from README/Tactic/Cong.agda rename to doc/README/Tactic/Cong.agda diff --git a/README/Tactic/MonoidSolver.agda b/doc/README/Tactic/MonoidSolver.agda similarity index 100% rename from README/Tactic/MonoidSolver.agda rename to doc/README/Tactic/MonoidSolver.agda diff --git a/README/Tactic/RingSolver.agda b/doc/README/Tactic/RingSolver.agda similarity index 100% rename from README/Tactic/RingSolver.agda rename to doc/README/Tactic/RingSolver.agda diff --git a/README/Text/Pretty.agda b/doc/README/Text/Pretty.agda similarity index 100% rename from README/Text/Pretty.agda rename to doc/README/Text/Pretty.agda diff --git a/README/Text/Printf.agda b/doc/README/Text/Printf.agda similarity index 100% rename from README/Text/Printf.agda rename to doc/README/Text/Printf.agda diff --git a/README/Text/Regex.agda b/doc/README/Text/Regex.agda similarity index 100% rename from README/Text/Regex.agda rename to doc/README/Text/Regex.agda diff --git a/README/Text/Tabular.agda b/doc/README/Text/Tabular.agda similarity index 100% rename from README/Text/Tabular.agda rename to doc/README/Text/Tabular.agda diff --git a/notes/installation-guide.md b/doc/installation-guide.md similarity index 100% rename from notes/installation-guide.md rename to doc/installation-guide.md diff --git a/notes/release-guide.txt b/doc/release-guide.txt similarity index 85% rename from notes/release-guide.txt rename to doc/release-guide.txt index 2f3f9d862f..0296bc0fe1 100644 --- a/notes/release-guide.txt +++ b/doc/release-guide.txt @@ -61,20 +61,12 @@ procedure should be followed: * Announce the release of the new version on the Agda mailing lists (users and developers). -* Add v$VERSION to the list of protected directories in the .travis.yml - file of BOTH master and experimental. They should look something like: - - > git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ (...) - - Commit & push these changes. This will prevent the next step from being - overwritten by travis. - * Generate and upload documentation for the released version: - cp travis/* . + cp .github/tooling/* . runhaskell GenerateEverything.hs ./index.sh - agda -i. -isrc --html index.agda + agda -i. -idoc -isrc --html index.agda mv html v$VERSION git checkout gh-pages git add v$VERSION/*.html v$VERSION/*.css diff --git a/doc/standard-library-doc.agda-lib b/doc/standard-library-doc.agda-lib new file mode 100644 index 0000000000..02aaaba402 --- /dev/null +++ b/doc/standard-library-doc.agda-lib @@ -0,0 +1,4 @@ +name: standard-library-doc +include: . ../src +flags: + --warning=noUnsupportedIndexedMatch diff --git a/notes/style-guide.md b/doc/style-guide.md similarity index 100% rename from notes/style-guide.md rename to doc/style-guide.md diff --git a/notes/updating-experimental.txt b/doc/updating-experimental.txt similarity index 100% rename from notes/updating-experimental.txt rename to doc/updating-experimental.txt diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml index 6f50570fcf..a12022572e 100644 --- a/fix-whitespace.yaml +++ b/fix-whitespace.yaml @@ -5,7 +5,6 @@ included-dirs: included-files: - "*.agda" - "*.md" - - ".travis.yml" excluded-files: - "README/Text/Tabular.agda"