[ fix #1743 ] move README to doc/ directory

.github/workflows/ci-ubuntu.yml

@@ -50,7 +50,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

GNUmakefile

@@ -9,23 +9,27 @@ 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
 
 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

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."
   ]
 
 

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)
 ===========================

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
 =========================

dev/.gitignore

@@ -0,0 +1 @@
+*

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/`.

dev/experimental.agda-lib

@@ -0,0 +1,4 @@
+name: standard-library-dev
+include: . ../src
+flags:
+  --warning=noUnsupportedIndexedMatch

README/Design/Hierarchies.agda → doc/README/Design/Hierarchies.agda

@@ -265,7 +265,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 --       IsA                     A
 --    /  ||   \               /  ||  \
 -- IsB   IsC   IsD          B    C    D
- 
+
 -- The procedure for re-exports in the bundles is as follows:
 
 -- 1. `open IsA isA public using (IsC, M)` where `M` is everything
@@ -280,7 +280,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 
 -- 5. `open B b public using (O)` where `O` is everything exported
 --    by `B` but not exported by `IsA`.
- 
+
 -- 6. Construct `d : D` via the `isC` obtained in step 1.
 
 -- 7. `open D d public using (P)` where `P` is everything exported

doc/standard-library-doc.agda-lib

@@ -0,0 +1,4 @@
+name: standard-library-doc
+include: . ../src
+flags:
+  --warning=noUnsupportedIndexedMatch

fix-whitespace.yaml

@@ -5,7 +5,6 @@ included-dirs:
 included-files:
   - "*.agda"
   - "*.md"
-  - ".travis.yml"
 
 excluded-files:
   - "README/Text/Tabular.agda"

notes/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

src/Effect/Applicative.agda

@@ -56,7 +56,7 @@ record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where
   -- Haskell-style alternative name for pure
   return : A → F A
   return = pure
-  
+
   -- backwards compatibility: unicode variants
   _⊛_ : F (A → B) → F A → F B
   _⊛_ = _<*>_

src/Function/Bundles.agda

@@ -380,7 +380,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   -- For further background on (split) surjections, one may consult any
   -- general mathematical references which work without the principle
   -- of choice. For example:
-  -- 
+  --
   --   https://ncatlab.org/nlab/show/split+epimorphism.
   --
   -- The connection to set-theoretic notions with the same names is