Updating existing tests, fixing treatment of DT parameters, WIP on em…

…acs leg.

WIP

[ Makefile ] goal continue-cubical-test;  update cubical submodule

Fix typo in CHANGELOG (agda#5905)

[ workflows ] fix stack/Win (ICU again) (agda#5909)

Stack was updated to MSYS2 2022-05-03 upstream.
This solved the keyring problem, but we need to reset the cache.

Provenance of where modules in Internal syntax.

Qualify some prelude functions in .ghci

Running stack repl failed due to these functions not being in scope

[ debug ] bump some verbosity levels

Fix agda#5901: use --batch when installing agda-mode for emacs

[ doc ] User-manual: installation: add agda to apt-get install

Replaces PR agda#5896 by @RosieBaish, thanks for the contribution.

User-manual: small improvements to section on `postulate` (agda#5916)

* [ doc ] User-manual: trick how to postulate sth in an expression
* [ doc ] remove silly `let open POSTULATE` trick again

[ cubical ] cosmetics: generalize iApplyVars

[ cosmetics ] turn absV (local def) into global def

[ cosmetics ] rewrite some TelView functions

Fixed agda#5920.

Re agda#5924: add LANGUAGE TypeOperators to pacify GHC 9.4

Re agda#5901: setup agda-mode: don't --no-site-file with --user

@nad reports errors with --no-site-file for agda-mode setup.

[ user-manual ] +example repeat for Streams, link copatterns->coinduction

Finish @RemcoSchrijver's PR agda#5918

[ re agda#5923 ] Don't apply rewrite rule instead of generating dummy terms when variables are not bound after matching

whitespacefix

wip

wip

wip

.ghci

@@ -41,8 +41,8 @@
 :def agda_load_local_ghci \_ -> do
   let localGhci = ".ghci.local"
   exists <- System.Directory.doesFileExist localGhci
-  return $ if exists
-    then ":script " ++ localGhci
+  Prelude.return Prelude.$ if exists
+    then ":script " Prelude.++ localGhci
     else ""
 :}
 :agda_load_local_ghci

.github/workflows/stack.yml

@@ -96,7 +96,7 @@ jobs:
     - with:
         path: ${{ steps.haskell-setup.outputs.stack-root }}
         key: |
-          ${{ runner.os }}-stack-00-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }}
+          ${{ runner.os }}-stack-20220503-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }}
       uses: actions/cache@v2
       name: Cache dependencies
       id: cache
@@ -112,7 +112,8 @@ jobs:
       name: Install the icu library (Ubuntu)
     - if: ${{ runner.os == 'Windows' }}
       run: |
-        stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring
+        stack exec ${ARGS} -- pacman --noconfirm -Syuu
+        # stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring
         stack exec ${ARGS} -- pacman --noconfirm -S ${ICU}
         stack exec ${ARGS} -- pacman --noconfirm -S mingw-w64-x86_64-pkg-config
       name: Install the icu library (Windows)

Agda.cabal

@@ -811,6 +811,7 @@ library
                     , StandaloneDeriving
                     , TupleSections
                     , TypeFamilies
+                    , TypeOperators
                     , TypeSynonymInstances
 
 executable agda
@@ -998,6 +999,7 @@ test-suite agda-tests
                      , StandaloneDeriving
                      , TupleSections
                      , TypeFamilies
+                     , TypeOperators
                      , TypeSynonymInstances
 
   if flag(optimise-heavily)

CHANGELOG.md

@@ -30,7 +30,7 @@ Language
   ([#4786](https://github.com/agda/agda/issues/4786)).
 
   For instance, the type of the constructor `c` below is now `{@0 A :
-  Set} → D A`, and the type of the record field `R.f` is {@0 A : Set}
+  Set} → D A`, and the type of the record field `R.f` is `{@0 A : Set}
   → R A → A`:
   ```agda
   data D (A : Set) : Set where

Makefile

@@ -526,6 +526,12 @@ cubical-test :
 		time $(MAKE) -C cubical \
                   AGDA_BIN=$(AGDA_BIN) RTS_OPTIONS=$(AGDA_OPTS))
 
+.PHONY : continue-cubical-test ##
+continue-cubical-test :
+	@$(call decorate, "Continuing cubical library test", \
+		time $(MAKE) -C cubical \
+                  AGDA_BIN=$(AGDA_BIN) RTS_OPTIONS=$(AGDA_OPTS))
+
 .PHONY : continue-std-lib-test ##
 continue-std-lib-test :
 	@(cd std-lib && \

doc/user-manual/getting-started/installation.rst

@@ -236,7 +236,7 @@ Prebuilt packages are available for Debian and Ubuntu from Karmic onwards. To in
 
 .. code-block:: bash
 
-  apt-get install agda-mode
+  apt-get install agda agda-mode
 
 This should install Agda and the Emacs mode.
 

doc/user-manual/language/coinduction.lagda.rst

@@ -58,11 +58,15 @@ constructor to the record type ``Stream``.
         fst : A
         snd : B
 
+Now we can use :ref:`copatterns <copatterns>` to create ``Stream``\s, like one that
+repeats a given element ``a`` infinitely many times::
 
-We can also define pointwise equality (a bisimulation and an equivalence) of a pair of ``Stream``\s as a
-coinductive record:
+    repeat : {A : Set} (a : A) -> Stream A
+    hd (repeat a) = a
+    tl (repeat a) = repeat a
 
-::
+We can also define pointwise equality (a bisimulation and an equivalence) of a pair of ``Stream``\s as a
+coinductive record::
 
     record _≈_ {A} (xs : Stream A) (ys : Stream A) : Set where
       coinductive
@@ -108,7 +112,6 @@ Finally, we can prove that ``merge`` is a left inverse for ``split``:
     tl-≈ (merge-split-id xs) = merge-split-id (tl xs)
 
 
-
 Old Coinduction
 ---------------
 

doc/user-manual/language/copatterns.lagda.rst

@@ -21,9 +21,10 @@
 Copatterns
 **********
 
-Consider the following record:
+.. note:: If you are looking for information on how to use copatterns with
+   coinductive records, please visit the section on :ref:`coinduction <coinduction>`.
 
-::
+Consider the following record::
 
   record Enumeration (A : Set) : Set where
     constructor enumeration
@@ -72,8 +73,8 @@ specify all the fields in a single expression:
     open Enumeration
 
     enum-Nat : Enumeration Nat
-    enum-Nat = record {
-        start    = 0
+    enum-Nat = record
+      { start    = 0
       ; forward  = suc
       ; backward = pred
       }
@@ -138,8 +139,8 @@ Without copatterns, we just add the extra argument to the function declaration:
     open Enumeration
 
     enum-Nat : Nat → Enumeration Nat
-    enum-Nat initial = record {
-        start    = initial
+    enum-Nat initial = record
+      { start    = initial
       ; forward  = suc
       ; backward = pred
       }
@@ -191,8 +192,8 @@ value to start with based on the user-provided flag:
     if false then _ else y = y
 
     enum-Nat : Bool → Enumeration Nat
-    enum-Nat ahead = record {
-        start    = if ahead then 42 else 0
+    enum-Nat ahead = record
+      { start    = if ahead then 42 else 0
       ; forward  = suc
       ; backward = pred
       }
@@ -266,4 +267,3 @@ With copatterns, we can do the case analysis directly by pattern matching:
        forward  enum-Nat n = suc n
        backward enum-Nat zero    = zero
        backward enum-Nat (suc n) = n
-

doc/user-manual/language/postulates.lagda.rst

@@ -25,7 +25,7 @@ Example: ::
     A B    : Set
     a      : A
     b      : B
-    _=AB=_ : A -> B -> Set
+    _=AB=_ : A → B → Set
     a==b   : a =AB= b
 
 Introducing postulates is in general not recommended. Once postulates are introduced the consistency of the whole development is at risk, because there is nothing that prevents us from introducing an element in the empty set.
@@ -36,21 +36,33 @@ Introducing postulates is in general not recommended. Once postulates are introd
 
   postulate bottom : False
 
-A preferable way to work is to define a module parametrised by the elements we need
+Postulates are forbidden in :ref:`Safe Agda <safe-agda>` (option :option:`--safe`) to prevent accidential inconsistencies.
 
-::
+A preferable way to work with assumptions is to define a module parametrised by the elements we need::
 
   module Absurd (bt : False) where
 
     -- ...
 
   module M (A B : Set) (a : A) (b : B)
-           (_=AB=_ : A -> B -> Set) (a==b : a =AB= b) where
+           (_=AB=_ : A → B → Set) (a==b : a =AB= b) where
 
     -- ...
 
 
 Postulated built-ins
 --------------------
 
-Some :ref:`built-ins` such as `Float` and `Char` are introduced as a postulate and then given a meaning by the corresponding ``{-# BUILTIN ... #-}`` pragma.
+Some :ref:`built-ins <built-ins>` such as `Float` and `Char` are introduced as a postulate and then given a meaning by the corresponding ``{-# BUILTIN ... #-}`` pragma.
+
+Local uses of ``postulate``
+---------------------------
+
+Postulates are declarations and can appear in positions where arbitrary declarations are allowed, e.g., in ``where`` blocks::
+
+  module PostulateInWhere where
+
+    my-theorem : (A : Set) → A
+    my-theorem A = I-prove-this-later
+      where
+        postulate I-prove-this-later : _

doc/user-manual/unicode-symbols-sphinx.tex.txt

@@ -259,6 +259,7 @@
 \DeclareUnicodeCharacter{2467}{\ensuremath{\text{\ding{179}}}} % Symbol ⑧
 \DeclareUnicodeCharacter{2468}{\ensuremath{\text{\ding{180}}}} % Symbol ⑨
 
+\DeclareUnicodeCharacter{25A1}{\ensuremath{\Box}}           % Symbol □
 \DeclareUnicodeCharacter{25C5}{\ensuremath{\triangleleft}}  % Symbol ◅
 
 \DeclareUnicodeCharacter{2660}{\ensuremath{\spadesuit}} % Symbol ♠

src/agda-mode/Main.hs

@@ -122,7 +122,7 @@ setupDotEmacs files = do
 -- | Tries to find the user's .emacs file by querying Emacs.
 
 findDotEmacs :: IO FilePath
-findDotEmacs = askEmacs "(insert (expand-file-name user-init-file))"
+findDotEmacs = askEmacs "(expand-file-name user-init-file)"
 
 -- | Has the Agda mode already been set up?
 
@@ -167,14 +167,24 @@ askEmacs query = do
           (removeFile . fst) $ \(file, h) -> do
     hClose h
     exit <- rawSystemWithDiagnostics "emacs"
-                      [ "--no-desktop", "-nw", "--no-splash"
-                          -- Andreas, 2014-01-11: ^ try a leaner startup of emacs
-                          -- Andreas, 2018-09-08: -nw instead of --no-window-system as some emacses do not support the long version
-                      , "--eval"
-                      , "(with-temp-file " ++ escape file ++ " "
-                                           ++ query ++ ")"
-                      , "--kill"
-                      ]
+      [ "--batch"
+          -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):
+          -- Use Emacs batch mode so that it can run without a terminal.
+      , "--user", ""
+          -- The flag --user is necessary with --batch so that user-init-file is defined.
+          -- The empty user is the default user.
+          -- (Option --batch includes --no-init-file, this is reverted by supplying --user.)
+      -- Andreas, 2022-05-25, issue #5901 reloaded:
+      -- Loading the init file without loading the site fails for some users:
+      -- , "--quick"
+      --     -- Option --quick includes --no-site-file.
+      , "--eval"
+      , apply [ "with-temp-file", escape file, apply [ "insert", query ] ]
+          -- Short cutting the temp file via just [ "princ", query ]
+          -- does not work if the loading of the user-init-file prints extra stuff.
+          -- Going via the temp file we can let this stuff go to stdout without
+          -- affecting the output we care about.
+      ]
     unless (exit == ExitSuccess) $ do
       informLn "Unable to query Emacs."
       exitFailure
@@ -249,16 +259,16 @@ compileElispFiles = do
   where
   compile dataDir f = do
     exit <- rawSystemWithDiagnostics "emacs" $
-                      [ "--no-init-file", "--no-site-file"
-                      , "--directory", dataDir
-                      , "--batch"
-                      , "--eval"
-                      , "(progn \
-                           \(setq byte-compile-error-on-warn t) \
-                           \(byte-compile-disable-warning 'cl-functions) \
-                           \(batch-byte-compile))"
-                      , f
-                      ]
+      [ "--quick"                -- 'quick' implies 'no-site-file'
+      , "--directory", dataDir
+      , "--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.
+      , "--eval"
+      , "(progn \
+           \(setq byte-compile-error-on-warn t) \
+           \(byte-compile-disable-warning 'cl-functions) \
+           \(batch-byte-compile))"
+      , f
+      ]
     return $ if exit == ExitSuccess then Nothing else Just f
 
 ------------------------------------------------------------------------
@@ -269,3 +279,10 @@ compileElispFiles = do
 
 inform   = hPutStr   stderr
 informLn = hPutStrLn stderr
+
+parens :: String -> String
+parens s = concat [ "(", s, ")" ]
+
+-- LISP application
+apply :: [String] -> String
+apply = parens . unwords

src/data/emacs-mode/agda2-mode.el

@@ -874,13 +874,18 @@ The action depends on the prefix argument:
 
 
 (defun agda2-intro-constructor-select (old-g choices)
-  "con select" ;; TODO : write description here
+  "Constructor select interface."
   (interactive)
-  (let* ((choicesLabels (mapcar (lambda (x) (propertize (car x) 'display (concat (car x) " : " (car (cdr x)) ) ))  choices))
+  (let* ((choicesLabels
+          (mapcar (lambda (x) (cons (car x) (propertize (concat " : " (car (cdr x))) 'face 'bold)))
+                  choices))
          (z (minibuffer-with-setup-hook 'minibuffer-complete
-               (completing-read "Constructor: " choicesLabels nil t)))
+              (let ((completion-extra-properties
+                     '(:annotation-function
+                        (lambda (candidate) (cdr (assoc candidate choicesLabels))))))
+                (completing-read "Constructor: " choicesLabels nil t))))
          (y (cdr (cdr (assoc z choices )))))
-    (if y (agda2-give-action old-g y))))
+    (if y (agda2-give-action old-g y) (force-mode-line-update))))
 
 
 (defun agda2-refine (pmlambda)

src/full/Agda/Auto/Auto.hs

@@ -382,12 +382,12 @@ auto ii rng argstr = liftTCM $ locallyTC eMakeCase (const True) $ do
             case cls' of
              Left{} -> stopWithMsg "No solution found"
              Right cls' -> do
-              cls'' <- forM cls' $ \ (I.Clause _ _ tel ps body t catchall exact recursive reachable ell) -> do
+              cls'' <- forM cls' $ \ (I.Clause _ _ tel ps body t catchall exact recursive reachable ell wm) -> do
                 withCurrentModule (AN.qnameModule def) $ do
                  -- Normalise the dot patterns
                  ps <- addContext tel $ normalise ps
                  body <- etaContract body
-                 fmap modifyAbstractClause $ inTopContext $ reify $ AN.QNamed def $ I.Clause noRange noRange tel ps body t catchall exact recursive reachable ell
+                 fmap modifyAbstractClause $ inTopContext $ reify $ AN.QNamed def $ I.Clause noRange noRange tel ps body t catchall exact recursive reachable ell wm
               moduleTel <- lookupSection (AN.qnameModule def)
               pcs <- withInteractionId ii $ inTopContext $ addContext moduleTel $ mapM prettyA cls''
               ticks <- liftIO $ readIORef ticks

src/full/Agda/Auto/Convert.hs

@@ -668,18 +668,19 @@ frommyClause (ids, pats, mrhs) = do
           Nothing -> return $ Nothing
           Just e -> Just <$> convert e
  let cperm =  Perm nv perm
- return $ I.Clause
+ return I.Clause
    { I.clauseLHSRange  = SP.noRange
    , I.clauseFullRange = SP.noRange
    , I.clauseTel       = tel
    , I.namedClausePats = IP.numberPatVars __IMPOSSIBLE__ cperm $ applySubst (renamingR $ compactP cperm) ps
-   , I.clauseBody  = body
-   , I.clauseType  = Nothing -- TODO: compute clause type
-   , I.clauseCatchall = False
+   , I.clauseBody      = body
+   , I.clauseType      = Nothing -- TODO: compute clause type
+   , I.clauseCatchall    = False
    , I.clauseExact       = Nothing -- TODO
    , I.clauseRecursive   = Nothing -- TODO: Don't know here whether recursive or not !?
    , I.clauseUnreachable = Nothing -- TODO: Don't know here whether reachable or not !?
-   , I.clauseEllipsis = Cm.NoEllipsis
+   , I.clauseEllipsis    = Cm.NoEllipsis
+   , I.clauseWhereModule = Nothing
    }
 
 contains_constructor :: [CSPat O] -> Bool