[Agda] Hoogle for Agda?
Philip Wadler
wadler at inf.ed.ac.uk
Fri Feb 16 14:06:27 CET 2018
Thanks!
There is a long run, ending with:
cabal exec -- GenerateEverything
cabal: The program 'GenerateEverything' is required but it could not be
found.
make: *** [Everything.agda] Error 1
bruichladdich$ ls
AllNonAsciiChars.hs Setup.hs
CHANGELOG.md dist
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
README.md
bruichladdich$
Which is mysterious, since as you can see, GenerateEverything.hs is
present. Complete run below, in case you want details. Fortunately, I have
a version copied from the html page cited earlier, which works well enough
for now. An easy way to fix the problem for the future is to check
Everything.agda into the repository, rather than leaving each user to
generate it for theirself. Cheers, -- P
bruichladdich$ cd ~/agda-stdlib/
bruichladdich$ ls
AllNonAsciiChars.hs README.md
CHANGELOG.md Setup.hs
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
bruichladdich$ git pull
remote: Counting objects: 17, done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 17 (delta 13), reused 17 (delta 13), pack-reused 0
Unpacking objects: 100% (17/17), done.
From https://github.com/agda/agda-stdlib
a68ee7e0..157497a5 master -> origin/master
81b74c8a..d8ae867e gh-pages -> origin/gh-pages
Updating a68ee7e0..157497a5
Fast-forward
CHANGELOG.md | 25 ++++++++++++-------------
src/Data/Table.agda | 6 +++---
src/Data/Table/Base.agda | 10 +++++-----
src/Data/Table/Properties.agda | 31 ++++++++++++++++---------------
src/Data/Table/Relation/Equality.agda | 4 ++--
5 files changed, 38 insertions(+), 38 deletions(-)
bruichladdich$ ls
AllNonAsciiChars.hs README.md
CHANGELOG.md Setup.hs
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
bruichladdich$ make Everything.agda
cabal clean && cabal install
cleaning...
Warning: --root-cmd is no longer supported, see
https://github.com/haskell/cabal/issues/3353 (if you didn't type --root-cmd,
comment out root-cmd in your ~/.cabal/config file)
Warning: The package list for 'hackage.haskell.org' is 63 days old.
Run 'cabal update' to get the latest list of available packages.
Resolving dependencies...
Downloading unix-compat-0.5.0.1...
Configuring unix-compat-0.5.0.1...
Preprocessing library for unix-compat-0.5.0.1..
Building library for unix-compat-0.5.0.1..
[1 of 8] Compiling System.PosixCompat.Files (
dist/build/System/PosixCompat/Files.hs,
dist/build/System/PosixCompat/Files.o )
[2 of 8] Compiling System.PosixCompat.Temp (
src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.o )
[3 of 8] Compiling System.PosixCompat.Time (
src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.o )
[4 of 8] Compiling System.PosixCompat.Types (
src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.o )
[5 of 8] Compiling System.PosixCompat.Extensions (
dist/build/System/PosixCompat/Extensions.hs,
dist/build/System/PosixCompat/Extensions.o )
[6 of 8] Compiling System.PosixCompat.Unistd (
src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.o )
[7 of 8] Compiling System.PosixCompat.User (
dist/build/System/PosixCompat/User.hs, dist/build/System/PosixCompat/User.o
)
[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs,
dist/build/System/PosixCompat.o )
[1 of 8] Compiling System.PosixCompat.Files (
dist/build/System/PosixCompat/Files.hs,
dist/build/System/PosixCompat/Files.p_o )
[2 of 8] Compiling System.PosixCompat.Temp (
src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.p_o )
[3 of 8] Compiling System.PosixCompat.Time (
src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.p_o )
[4 of 8] Compiling System.PosixCompat.Types (
src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.p_o )
[5 of 8] Compiling System.PosixCompat.Extensions (
dist/build/System/PosixCompat/Extensions.hs,
dist/build/System/PosixCompat/Extensions.p_o )
[6 of 8] Compiling System.PosixCompat.Unistd (
src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.p_o )
[7 of 8] Compiling System.PosixCompat.User (
dist/build/System/PosixCompat/User.hs,
dist/build/System/PosixCompat/User.p_o )
[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs,
dist/build/System/PosixCompat.p_o )
Preprocessing library for unix-compat-0.5.0.1..
Running Haddock on library for unix-compat-0.5.0.1..
Haddock coverage:
99% ( 77 / 78) in 'System.PosixCompat.Files'
Missing documentation for:
PathVar
100% ( 2 / 2) in 'System.PosixCompat.Temp'
100% ( 2 / 2) in 'System.PosixCompat.Time'
100% ( 2 / 2) in 'System.PosixCompat.Types'
71% ( 5 / 7) in 'System.PosixCompat.Extensions'
Missing documentation for:
CMajor (src/System/PosixCompat/Extensions.hsc:23)
CMinor (src/System/PosixCompat/Extensions.hsc:24)
75% ( 6 / 8) in 'System.PosixCompat.Unistd'
Missing documentation for:
SystemID
getSystemID
91% ( 21 / 23) in 'System.PosixCompat.User'
Missing documentation for:
GroupEntry
UserEntry
100% ( 8 / 8) in 'System.PosixCompat'
Documentation created: dist/doc/html/unix-compat/index.html
Installing library in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/unix-compat-0.5.0.1/lib
Installed unix-compat-0.5.0.1
Downloading filemanip-0.3.6.3...
Configuring filemanip-0.3.6.3...
Preprocessing library for filemanip-0.3.6.3..
Building library for filemanip-0.3.6.3..
[1 of 4] Compiling System.FilePath.GlobPattern (
System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.o )
System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs,
dist/build/System/FilePath/Glob.o )
[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs,
dist/build/System/FilePath/Find.o )
System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^
System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^
System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^
System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^
System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^
System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^
System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^
System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs,
dist/build/System/FilePath/Manip.o )
[1 of 4] Compiling System.FilePath.GlobPattern (
System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.p_o )
System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs,
dist/build/System/FilePath/Glob.p_o )
[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs,
dist/build/System/FilePath/Find.p_o )
System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^
System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^
System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^
System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^
System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^
System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^
System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^
System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs,
dist/build/System/FilePath/Manip.p_o )
Preprocessing library for filemanip-0.3.6.3..
Running Haddock on library for filemanip-0.3.6.3..
Haddock coverage:
System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
100% ( 7 / 7) in 'System.FilePath.GlobPattern'
100% ( 2 / 2) in 'System.FilePath.Glob'
System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^
System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^
System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^
System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^
System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^
System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^
System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^
System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^
System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^
System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
65% ( 41 / 63) in 'System.FilePath.Find'
Missing documentation for:
FileType (System/FilePath/Find.hs:394)
FilterPredicate (System/FilePath/Find.hs:202)
RecursionPredicate (System/FilePath/Find.hs:203)
deviceID (System/FilePath/Find.hs:439)
fileID (System/FilePath/Find.hs:442)
fileOwner (System/FilePath/Find.hs:445)
fileGroup (System/FilePath/Find.hs:448)
fileSize (System/FilePath/Find.hs:451)
linkCount (System/FilePath/Find.hs:454)
specialDeviceID (System/FilePath/Find.hs:457)
fileMode (System/FilePath/Find.hs:460)
accessTime (System/FilePath/Find.hs:478)
modificationTime (System/FilePath/Find.hs:481)
statusChangeTime (System/FilePath/Find.hs:484)
==? (System/FilePath/Find.hs:527)
/=? (System/FilePath/Find.hs:531)
>? (System/FilePath/Find.hs:535)
<? (System/FilePath/Find.hs:539)
>=? (System/FilePath/Find.hs:543)
<=? (System/FilePath/Find.hs:547)
&&? (System/FilePath/Find.hs:557)
||? (System/FilePath/Find.hs:561)
100% ( 6 / 6) in 'System.FilePath.Manip'
Documentation created: dist/doc/html/filemanip/index.html
Installing library in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/filemanip-0.3.6.3/lib
Installed filemanip-0.3.6.3
Configuring lib-0.14...
Preprocessing executable 'GenerateEverything' for lib-0.14..
Building executable 'GenerateEverything' for lib-0.14..
[1 of 1] Compiling Main ( GenerateEverything.hs,
dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )
Linking dist/build/GenerateEverything/GenerateEverything ...
Preprocessing executable 'AllNonAsciiChars' for lib-0.14..
Building executable 'AllNonAsciiChars' for lib-0.14..
[1 of 1] Compiling Main ( AllNonAsciiChars.hs,
dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )
Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...
Warning: No documentation was generated as this package does not contain a
library. Perhaps you want to use the --executables, --tests, --benchmarks or
--foreign-libraries flags.
Installing executable GenerateEverything in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin
Warning: The directory
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the
system
search path.
Installing executable AllNonAsciiChars in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin
Warning: The directory
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the
system
search path.
Installed lib-0.14
Updating documentation index /Users/wadler/Library/Haskell/doc/index.html
cabal exec -- GenerateEverything
cabal: The program 'GenerateEverything' is required but it could not be
found.
make: *** [Everything.agda] Error 1
bruichladdich$ ls
AllNonAsciiChars.hs Setup.hs
CHANGELOG.md dist
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
README.md
bruichladdich$
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
On 15 February 2018 at 22:00, Liam O'Connor <liamoc at cse.unsw.edu.au> wrote:
> Hi Phil,
>
> Sorry, the Makefile is called GNUmakefile. it’s here, for future reference:
>
> https://github.com/agda/agda-stdlib/blob/master/GNUmakefile
>
> I think, if you have GNU make, “make Everything.agda” should work.
>
> L
>
> On 16 February 2018 at 6:08:18 am, Philip Wadler (wadler at inf.ed.ac.uk)
> wrote:
>
> Thank you! Everything sounds like everything I need!
>
> I got the standard library from here:
>
> git clone https://github.com/agda/agda-stdlib.git ~/agda-stdlib
>
> This version does not have a file called Everything. It has no Makefile
> that I can spot. It does contain a file called GenerateEverything.hs, but
> it doesn't work for me:
>
> bruichladdich$ ghci GenerateEverything.hs
>> GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
>> [1 of 1] Compiling Main ( GenerateEverything.hs, interpreted )
>> GenerateEverything.hs:9:1: error:
>> Could not find module ‘System.FilePath.Find’
>> Perhaps you meant
>> System.FilePath.Windows (from filepath-1.4.1.2)
>> System.FilePath (from filepath-1.4.1.2)
>> System.FilePath.Posix (from filepath-1.4.1.2)
>> Use -v to see a list of the files searched for.
>> |
>> 9 | import System.FilePath.Find
>> | ^^^^^^^^^^^^^^^^^^^^^^^^^^^
>> Failed, no modules loaded.
>> Prelude>
>
>
> What are my other options? Could someone simply add Everything.agda to
> https://github.com/agda/agda-stdlib.git, and then I could pull it?
>
> Cheers, -- P
>
>
>
>
> . \ Philip Wadler, Professor of Theoretical Computer Science,
> . /\ School of Informatics, University of Edinburgh
> . / \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 15 February 2018 at 14:23, Liam O'Connor <liamoc at cse.unsw.edu.au>
> wrote:
>
>>
>> The agda standard library has a makefile entry for an “Everything.agda”
>> that includes.. well… everything in the standard library.
>>
>> You can build that file, and it should suit your purposes. (It has a
>> listing here http://www.cse.chalmers.se/~nad/listings/lib/Everything.html
>> )
>>
>> Regards,
>> Liam
>>
>> On 16 February 2018 at 3:19:04 am, Philip Wadler (wadler at inf.ed.ac.uk)
>> wrote:
>>
>> Thanks!
>>
>> What would help enormously is if I could do the same thing, *searching
>> the entire standard library*. This basically requires someone to put
>> together a huge import list and put it in a file (preferably available with
>> the standard library). Has anyone done so, or could this be whipped
>> together quickly?
>>
>> Cheers, -- P
>>
>> . \ Philip Wadler, Professor of Theoretical Computer Science,
>> . /\ School of Informatics, University of Edinburgh
>> . / \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> On 15 February 2018 at 14:01, Guillaume Allais <
>> guillaume.allais at ens-lyon.org> wrote:
>>
>>> Hi Phil,
>>>
>>> There's a *very basic* search functionality which you can invoke
>>> from emacs using C-c C-z. You can then input a space-separated
>>> list of identifiers and strings and Agda will return all the
>>> identifiers which:
>>> - are in scope in the current module
>>> - contain in their type *all* of the identifiers mentioned
>>> - contain as substring *all* of the mentioned strings
>>>
>>> For instance, using a fairly recent version of the stdlib, from
>>> the module containing:
>>>
>>> ===========================================
>>> open import Data.Nat
>>> open import Data.Nat.Properties
>>> ===========================================
>>>
>>> C-c C-z RET _+_ _*_ RET
>>>
>>> will return
>>>
>>> ===========================================
>>> Definitions about _+_, _*_
>>> *-+-isCommutativeSemiring
>>> : .Algebra.Structures.IsCommutativeSemiring
>>> .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
>>> *-cancelˡ-≡
>>> : {i j : ℕ} (k : ℕ) →
>>> i + k * i .Agda.Builtin.Equality.≡ j + k * j →
>>> i .Agda.Builtin.Equality.≡ j
>>> *-distrib-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOver _*_)
>>> _+_
>>> *-distribʳ-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverʳ _*_)
>>> _+_
>>> *-distribˡ-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverˡ _*_)
>>> _+_
>>> +-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m + m * n
>>> ^-distribˡ-+-*
>>> : (m n p : ℕ) →
>>> (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
>>> distribʳ-*-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverʳ _*_)
>>> _+_
>>> im≡jm+n⇒[i∸j]m≡n
>>> : (i j m n : ℕ) →
>>> i * m .Agda.Builtin.Equality.≡ j * m + n →
>>> (i ∸ j) * m .Agda.Builtin.Equality.≡ n
>>> isCommutativeSemiring
>>> : .Algebra.Structures.IsCommutativeSemiring
>>> .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
>>> ===========================================
>>>
>>> and C-c C-z RET _+_ _*_ "distr" RET
>>> will filter definitions which are not about distributivity:
>>>
>>> ===========================================
>>> Definitions about _+_, _*_, "distr"
>>> *-distrib-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOver _*_)
>>> _+_
>>> *-distribʳ-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverʳ _*_)
>>> _+_
>>> *-distribˡ-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverˡ _*_)
>>> _+_
>>> ^-distribˡ-+-*
>>> : (m n p : ℕ) →
>>> (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
>>> distribʳ-*-+
>>> : (.Agda.Builtin.Equality._≡_
>>> .Algebra.FunctionProperties.DistributesOverʳ _*_)
>>> _+_
>>> ===========================================
>>>
>>> This search function respect the normalisation modifiers (that
>>> is the (C-u)* you can type before most commands) and will search
>>> types according to the normalisation level you've requested (and
>>> print results accordingly).
>>>
>>> Cheers,
>>> --
>>> gallais
>>>
>>>
>>> On 15/02/18 16:52, Philip Wadler wrote:
>>>
>>> Is there anything like Hoogle for Agda? It would save newbies like me a
>>> *lot* of time. Cheers, -- P
>>>
>>> . \ Philip Wadler, Professor of Theoretical Computer Science,
>>> . /\ School of Informatics, University of Edinburgh
>>> . / \ and Senior Research Fellow, IOHK
>>> . http://homepages.inf.ed.ac.uk/wadler/
>>>
>>>
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/9d4faaf0/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/9d4faaf0/attachment-0001.ksh>
More information about the Agda
mailing list