<div dir="ltr">Thanks!<div><br></div><div>There is a long run, ending with:</div><div><br></div><div><div>cabal exec -- GenerateEverything</div><div>cabal: The program 'GenerateEverything' is required but it could not be found.</div><div>make: *** [Everything.agda] Error 1</div><div>bruichladdich$ ls</div><div>AllNonAsciiChars.hs<span style="white-space:pre"> </span>Setup.hs</div><div>CHANGELOG.md<span style="white-space:pre"> </span>dist</div><div>GNUmakefile<span style="white-space:pre"> </span>index.agda</div><div>GenerateEverything.hs<span style="white-space:pre"> </span>index.sh</div><div>HACKING.md<span style="white-space:pre"> </span>lib.cabal</div><div>Header<span style="white-space:pre"> </span>notes</div><div>LICENCE<span style="white-space:pre"> </span>publish-listings.sh</div><div>README<span style="white-space:pre"> </span>src</div><div>README.agda<span style="white-space:pre"> </span>standard-library.agda-lib</div><div>README.md</div><div>bruichladdich$ </div></div><div><br></div><div>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</div><div><br></div><div><br></div><div><div>bruichladdich$ cd ~/agda-stdlib/</div><div>bruichladdich$ ls</div><div>AllNonAsciiChars.hs<span style="white-space:pre"> </span>README.md</div><div>CHANGELOG.md<span style="white-space:pre"> </span>Setup.hs</div><div>GNUmakefile<span style="white-space:pre"> </span>index.agda</div><div>GenerateEverything.hs<span style="white-space:pre"> </span>index.sh</div><div>HACKING.md<span style="white-space:pre"> </span>lib.cabal</div><div>Header<span style="white-space:pre"> </span>notes</div><div>LICENCE<span style="white-space:pre"> </span>publish-listings.sh</div><div>README<span style="white-space:pre"> </span>src</div><div>README.agda<span style="white-space:pre"> </span>standard-library.agda-lib</div><div>bruichladdich$ git pull</div><div>remote: Counting objects: 17, done.</div><div>remote: Compressing objects: 100% (3/3), done.</div><div>remote: Total 17 (delta 13), reused 17 (delta 13), pack-reused 0</div><div>Unpacking objects: 100% (17/17), done.</div><div>From <a href="https://github.com/agda/agda-stdlib">https://github.com/agda/agda-stdlib</a></div><div> a68ee7e0..157497a5 master -> origin/master</div><div> 81b74c8a..d8ae867e gh-pages -> origin/gh-pages</div><div>Updating a68ee7e0..157497a5</div><div>Fast-forward</div><div> CHANGELOG.md | 25 ++++++++++++-------------</div><div> src/Data/Table.agda | 6 +++---</div><div> src/Data/Table/Base.agda | 10 +++++-----</div><div> src/Data/Table/Properties.agda | 31 ++++++++++++++++---------------</div><div> src/Data/Table/Relation/Equality.agda | 4 ++--</div><div> 5 files changed, 38 insertions(+), 38 deletions(-)</div><div>bruichladdich$ ls</div><div>AllNonAsciiChars.hs<span style="white-space:pre"> </span>README.md</div><div>CHANGELOG.md<span style="white-space:pre"> </span>Setup.hs</div><div>GNUmakefile<span style="white-space:pre"> </span>index.agda</div><div>GenerateEverything.hs<span style="white-space:pre"> </span>index.sh</div><div>HACKING.md<span style="white-space:pre"> </span>lib.cabal</div><div>Header<span style="white-space:pre"> </span>notes</div><div>LICENCE<span style="white-space:pre"> </span>publish-listings.sh</div><div>README<span style="white-space:pre"> </span>src</div><div>README.agda<span style="white-space:pre"> </span>standard-library.agda-lib</div><div>bruichladdich$ make Everything.agda</div><div>cabal clean && cabal install</div><div>cleaning...</div><div>Warning: --root-cmd is no longer supported, see</div><div><a href="https://github.com/haskell/cabal/issues/3353">https://github.com/haskell/cabal/issues/3353</a> (if you didn't type --root-cmd,</div><div>comment out root-cmd in your ~/.cabal/config file)</div><div>Warning: The package list for '<a href="http://hackage.haskell.org">hackage.haskell.org</a>' is 63 days old.</div><div>Run 'cabal update' to get the latest list of available packages.</div><div>Resolving dependencies...</div><div>Downloading unix-compat-0.5.0.1...</div><div>Configuring unix-compat-0.5.0.1...</div><div>Preprocessing library for unix-compat-0.5.0.1..</div><div>Building library for unix-compat-0.5.0.1..</div><div>[1 of 8] Compiling System.PosixCompat.Files ( dist/build/System/PosixCompat/Files.hs, dist/build/System/PosixCompat/Files.o )</div><div>[2 of 8] Compiling System.PosixCompat.Temp ( src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.o )</div><div>[3 of 8] Compiling System.PosixCompat.Time ( src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.o )</div><div>[4 of 8] Compiling System.PosixCompat.Types ( src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.o )</div><div>[5 of 8] Compiling System.PosixCompat.Extensions ( dist/build/System/PosixCompat/Extensions.hs, dist/build/System/PosixCompat/Extensions.o )</div><div>[6 of 8] Compiling System.PosixCompat.Unistd ( src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.o )</div><div>[7 of 8] Compiling System.PosixCompat.User ( dist/build/System/PosixCompat/User.hs, dist/build/System/PosixCompat/User.o )</div><div>[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs, dist/build/System/PosixCompat.o )</div><div>[1 of 8] Compiling System.PosixCompat.Files ( dist/build/System/PosixCompat/Files.hs, dist/build/System/PosixCompat/Files.p_o )</div><div>[2 of 8] Compiling System.PosixCompat.Temp ( src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.p_o )</div><div>[3 of 8] Compiling System.PosixCompat.Time ( src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.p_o )</div><div>[4 of 8] Compiling System.PosixCompat.Types ( src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.p_o )</div><div>[5 of 8] Compiling System.PosixCompat.Extensions ( dist/build/System/PosixCompat/Extensions.hs, dist/build/System/PosixCompat/Extensions.p_o )</div><div>[6 of 8] Compiling System.PosixCompat.Unistd ( src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.p_o )</div><div>[7 of 8] Compiling System.PosixCompat.User ( dist/build/System/PosixCompat/User.hs, dist/build/System/PosixCompat/User.p_o )</div><div>[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs, dist/build/System/PosixCompat.p_o )</div><div>Preprocessing library for unix-compat-0.5.0.1..</div><div>Running Haddock on library for unix-compat-0.5.0.1..</div><div>Haddock coverage:</div><div> 99% ( 77 / 78) in 'System.PosixCompat.Files'</div><div> Missing documentation for:</div><div> PathVar</div><div> 100% ( 2 / 2) in 'System.PosixCompat.Temp'</div><div> 100% ( 2 / 2) in 'System.PosixCompat.Time'</div><div> 100% ( 2 / 2) in 'System.PosixCompat.Types'</div><div> 71% ( 5 / 7) in 'System.PosixCompat.Extensions'</div><div> Missing documentation for:</div><div> CMajor (src/System/PosixCompat/Extensions.hsc:23)</div><div> CMinor (src/System/PosixCompat/Extensions.hsc:24)</div><div> 75% ( 6 / 8) in 'System.PosixCompat.Unistd'</div><div> Missing documentation for:</div><div> SystemID</div><div> getSystemID</div><div> 91% ( 21 / 23) in 'System.PosixCompat.User'</div><div> Missing documentation for:</div><div> GroupEntry</div><div> UserEntry</div><div> 100% ( 8 / 8) in 'System.PosixCompat'</div><div>Documentation created: dist/doc/html/unix-compat/index.html</div><div>Installing library in /Users/wadler/Library/Haskell/ghc-8.2.2/lib/unix-compat-0.5.0.1/lib</div><div>Installed unix-compat-0.5.0.1</div><div>Downloading filemanip-0.3.6.3...</div><div>Configuring filemanip-0.3.6.3...</div><div>Preprocessing library for filemanip-0.3.6.3..</div><div>Building library for filemanip-0.3.6.3..</div><div>[1 of 4] Compiling System.FilePath.GlobPattern ( System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.o )</div><div><br></div><div>System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]</div><div> This binding for ‘g’ shadows the existing binding</div><div> bound at System/FilePath/GlobPattern.hs:148:24</div><div> |</div><div>149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs</div><div> | ^</div><div>[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs, dist/build/System/FilePath/Glob.o )</div><div>[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs, dist/build/System/FilePath/Find.o )</div><div><br></div><div>System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>227 | where visit path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>238 | filterPath path depth st result =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:279:18</div><div> |</div><div>282 | in state' `seq` flip foldM state' (\state name -></div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>284 | let path = dir </> name</div><div> | ^^^^</div><div>[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs, dist/build/System/FilePath/Manip.o )</div><div>[1 of 4] Compiling System.FilePath.GlobPattern ( System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.p_o )</div><div><br></div><div>System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]</div><div> This binding for ‘g’ shadows the existing binding</div><div> bound at System/FilePath/GlobPattern.hs:148:24</div><div> |</div><div>149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs</div><div> | ^</div><div>[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs, dist/build/System/FilePath/Glob.p_o )</div><div>[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs, dist/build/System/FilePath/Find.p_o )</div><div><br></div><div>System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>227 | where visit path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>238 | filterPath path depth st result =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:279:18</div><div> |</div><div>282 | in state' `seq` flip foldM state' (\state name -></div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>284 | let path = dir </> name</div><div> | ^^^^</div><div>[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs, dist/build/System/FilePath/Manip.p_o )</div><div>Preprocessing library for filemanip-0.3.6.3..</div><div>Running Haddock on library for filemanip-0.3.6.3..</div><div>Haddock coverage:</div><div><br></div><div>System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]</div><div> This binding for ‘g’ shadows the existing binding</div><div> bound at System/FilePath/GlobPattern.hs:148:24</div><div> |</div><div>149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs</div><div> | ^</div><div> 100% ( 7 / 7) in 'System.FilePath.GlobPattern'</div><div> 100% ( 2 / 2) in 'System.FilePath.Glob'</div><div><br></div><div>System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>227 | where visit path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>231 | traverse dir depth dirSt = do</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>238 | filterPath path depth st result =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^</div><div><br></div><div>System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>274 | where visit state path depth st =</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]</div><div> This binding for ‘traverse’ shadows the existing binding</div><div> imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27</div><div> (and originally defined in ‘Data.Traversable’)</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:38</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]</div><div> This binding for ‘depth’ shadows the existing binding</div><div> defined at System/FilePath/Find.hs:195:1</div><div> |</div><div>279 | traverse state dir depth dirSt = handle (errHandler dir state) $</div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]</div><div> This binding for ‘state’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:279:18</div><div> |</div><div>282 | in state' `seq` flip foldM state' (\state name -></div><div> | ^^^^^</div><div><br></div><div>System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]</div><div> This binding for ‘path’ shadows the existing binding</div><div> bound at System/FilePath/Find.hs:271:44</div><div> |</div><div>284 | let path = dir </> name</div><div> | ^^^^</div><div> 65% ( 41 / 63) in 'System.FilePath.Find'</div><div> Missing documentation for:</div><div> FileType (System/FilePath/Find.hs:394)</div><div> FilterPredicate (System/FilePath/Find.hs:202)</div><div> RecursionPredicate (System/FilePath/Find.hs:203)</div><div> deviceID (System/FilePath/Find.hs:439)</div><div> fileID (System/FilePath/Find.hs:442)</div><div> fileOwner (System/FilePath/Find.hs:445)</div><div> fileGroup (System/FilePath/Find.hs:448)</div><div> fileSize (System/FilePath/Find.hs:451)</div><div> linkCount (System/FilePath/Find.hs:454)</div><div> specialDeviceID (System/FilePath/Find.hs:457)</div><div> fileMode (System/FilePath/Find.hs:460)</div><div> accessTime (System/FilePath/Find.hs:478)</div><div> modificationTime (System/FilePath/Find.hs:481)</div><div> statusChangeTime (System/FilePath/Find.hs:484)</div><div> ==? (System/FilePath/Find.hs:527)</div><div> /=? (System/FilePath/Find.hs:531)</div><div> >? (System/FilePath/Find.hs:535)</div><div> <? (System/FilePath/Find.hs:539)</div><div> >=? (System/FilePath/Find.hs:543)</div><div> <=? (System/FilePath/Find.hs:547)</div><div> &&? (System/FilePath/Find.hs:557)</div><div> ||? (System/FilePath/Find.hs:561)</div><div> 100% ( 6 / 6) in 'System.FilePath.Manip'</div><div>Documentation created: dist/doc/html/filemanip/index.html</div><div>Installing library in /Users/wadler/Library/Haskell/ghc-8.2.2/lib/filemanip-0.3.6.3/lib</div><div>Installed filemanip-0.3.6.3</div><div>Configuring lib-0.14...</div><div>Preprocessing executable 'GenerateEverything' for lib-0.14..</div><div>Building executable 'GenerateEverything' for lib-0.14..</div><div>[1 of 1] Compiling Main ( GenerateEverything.hs, dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )</div><div>Linking dist/build/GenerateEverything/GenerateEverything ...</div><div>Preprocessing executable 'AllNonAsciiChars' for lib-0.14..</div><div>Building executable 'AllNonAsciiChars' for lib-0.14..</div><div>[1 of 1] Compiling Main ( AllNonAsciiChars.hs, dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )</div><div>Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...</div><div>Warning: No documentation was generated as this package does not contain a</div><div>library. Perhaps you want to use the --executables, --tests, --benchmarks or</div><div>--foreign-libraries flags.</div><div>Installing executable GenerateEverything in /Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin</div><div>Warning: The directory</div><div>/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the system</div><div>search path.</div><div>Installing executable AllNonAsciiChars in /Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin</div><div>Warning: The directory</div><div>/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the system</div><div>search path.</div><div>Installed lib-0.14</div><div>Updating documentation index /Users/wadler/Library/Haskell/doc/index.html</div><div>cabal exec -- GenerateEverything</div><div>cabal: The program 'GenerateEverything' is required but it could not be found.</div><div>make: *** [Everything.agda] Error 1</div><div>bruichladdich$ ls</div><div>AllNonAsciiChars.hs<span style="white-space:pre"> </span>Setup.hs</div><div>CHANGELOG.md<span style="white-space:pre"> </span>dist</div><div>GNUmakefile<span style="white-space:pre"> </span>index.agda</div><div>GenerateEverything.hs<span style="white-space:pre"> </span>index.sh</div><div>HACKING.md<span style="white-space:pre"> </span>lib.cabal</div><div>Header<span style="white-space:pre"> </span>notes</div><div>LICENCE<span style="white-space:pre"> </span>publish-listings.sh</div><div>README<span style="white-space:pre"> </span>src</div><div>README.agda<span style="white-space:pre"> </span>standard-library.agda-lib</div><div>README.md</div><div>bruichladdich$ </div></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 15 February 2018 at 22:00, Liam O'Connor <span dir="ltr"><<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div id="m_-9127758530710006032bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">Hi Phil,</div><div id="m_-9127758530710006032bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto"><br></div><div id="m_-9127758530710006032bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">Sorry, the Makefile is called GNUmakefile. it’s here, for future reference:</div><div id="m_-9127758530710006032bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto"><br></div><div id="m_-9127758530710006032bloop_customfont" style="margin:0px"><a href="https://github.com/agda/agda-stdlib/blob/master/GNUmakefile" target="_blank">https://github.com/agda/agda-<wbr>stdlib/blob/master/GNUmakefile</a></div><div id="m_-9127758530710006032bloop_customfont" style="margin:0px"><br></div><div id="m_-9127758530710006032bloop_customfont" style="margin:0px">I think, if you have GNU make, “make Everything.agda” should work.</div><span class="HOEnZb"><font color="#888888"><div id="m_-9127758530710006032bloop_customfont" style="margin:0px"><br></div><div id="m_-9127758530710006032bloop_customfont" style="margin:0px">L</div></font></span><div><div class="h5"><p class="m_-9127758530710006032airmail_on">On 16 February 2018 at 6:08:18 am, Philip Wadler (<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>) wrote:</p> <blockquote type="cite" class="m_-9127758530710006032clean_bq"><span><div><div></div><div>
<div dir="ltr">Thank you! Everything sounds like everything I need!
<div><br></div>
<div>I got the standard library from here:</div>
<div><br></div>
<div> git clone <a href="https://github.com/agda/agda-stdlib.git" target="_blank">https://github.com/agda/<wbr>agda-stdlib.git</a> ~/agda-stdlib</div>
<div><br></div>
<div>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:</div>
<div><br></div>
<div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
bruichladdich$ ghci GenerateEverything.hs <br>
GHCi, version 8.2.2: <a href="http://www.haskell.org/ghc/" target="_blank">http://www.haskell.org/ghc/</a>
:? for help<br>
[1 of 1] Compiling Main
( GenerateEverything.hs, interpreted )<br>
GenerateEverything.hs:9:1: error:<br>
Could not find module ‘System.FilePath.Find’<br>
Perhaps you meant<br>
System.FilePath.Windows (from
filepath-1.4.1.2)<br>
System.FilePath (from filepath-1.4.1.2)<br>
System.FilePath.Posix (from
filepath-1.4.1.2)<br>
Use -v to see a list of the files searched for.<br>
|<br>
9 | import System.FilePath.Find<br>
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^<br>
Failed, no modules loaded.<br>
Prelude> </blockquote>
<div><br></div>
<div>What are my other options? Could someone simply add
Everything.agda to <a href="https://github.com/agda/agda-stdlib.git" style="color:rgb(17,85,204);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)" target="_blank">https://github.com/agda/agd<wbr>a-stdlib.git</a>,
and then I could pull it?</div>
<div><br></div>
<div>Cheers, -- P</div>
<blockquote type="cite" style="color:rgb(80,0,80);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">
<div class="gmail_extra">
<div class="gmail_quote">
<div><span style="font-size:small;color:rgb(34,34,34)"> </span><br></div>
</div>
</div>
</blockquote>
</div>
</div>
<div class="gmail_extra"><br clear="all">
<div>
<div class="m_-9127758530710006032gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical
Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br></div>
<div>. / \ and Senior Research Fellow, IOHK<br></div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 15 February 2018 at 14:23, Liam
O'Connor <span dir="ltr"><<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word;line-break:after-white-space">
<div id="m_-9127758530710006032m_-7173118898084949436bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<br></div>
The agda standard library has a makefile entry for an
“Everything.agda” that includes.. well… everything in the standard
library.
<div><br></div>
<div>You can build that file, and it should suit your purposes. (It
has a listing here <a href="http://www.cse.chalmers.se/~nad/listings/lib/Everything.html" target="_blank">http://www.cse.chalmers.s<wbr>e/~nad/listings/lib/Everything<wbr>.html</a>)</div>
<div><br>
<div class="m_-9127758530710006032m_-7173118898084949436bloop_sign" id="m_-9127758530710006032m_-7173118898084949436bloop_sign_1518711709732366080"></div>
<div id="m_-9127758530710006032m_-7173118898084949436bloop_sign_1518711709732366080" class="m_-9127758530710006032m_-7173118898084949436bloop_sign">Regards,</div>
<div id="m_-9127758530710006032m_-7173118898084949436bloop_sign_1518711709732366080" class="m_-9127758530710006032m_-7173118898084949436bloop_sign">Liam</div>
<div>
<div class="m_-9127758530710006032h5"><br>
<p class="m_-9127758530710006032m_-7173118898084949436airmail_on">On 16 February 2018 at
3:19:04 am, Philip Wadler (<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>) wrote:</p>
<blockquote type="cite" class="m_-9127758530710006032m_-7173118898084949436clean_bq">
<div>
<div>
<div dir="ltr"><span>Thanks!</span>
<div><span><br></span></div>
<div><span>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?</span></div>
<div><span><br></span></div>
<div><span>Cheers, -- P</span></div>
</div>
<div class="gmail_extra"><span><br clear="all"></span>
<div>
<div class="m_-9127758530710006032m_-7173118898084949436gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr"><span>. \ Philip Wadler, Professor of
Theoretical Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br></span></div>
<div><span>. / \ and Senior Research Fellow,
IOHK<br></span></div>
<div dir="ltr"><span>. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 15 February 2018 at 14:01, Guillaume
Allais <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a><wbr>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF"><tt>Hi Phil,<br>
<br>
There's a *very basic* search functionality which you can
invoke<br>
from emacs using C-c C-z. You can then input a
space-separated<br>
list of identifiers and strings and Agda will return all the<br>
identifiers which:<br>
- are in scope in the current module<br>
- contain in their type *all* of the identifiers mentioned<br>
- contain as substring *all* of the mentioned strings<br>
<br>
For instance, using a fairly recent version of the stdlib,
from<br>
the module containing:<br>
<br>
==============================<wbr>=============<br>
open import Data.Nat<br>
open import Data.Nat.Properties</tt><br>
<tt><tt>==============================<wbr>=============</tt><br>
<br>
C-c C-z RET _+_ _*_ RET<br>
<br>
will return<br>
<br></tt>
<tt><tt>==============================<wbr>=============<br>
Definitions about _+_, _*_<br>
*-+-isCommutativeSemiring<br>
:
.Algebra.Structures.IsCommutat<wbr>iveSemiring<br>
.Agda.Builtin.Equality._≡_ _+_ _*_ 0 1<br>
*-cancelˡ-≡<br>
: {i j : ℕ}
(k : ℕ) →<br>
i + k * i .Agda.Builtin.Equality.≡ j + k * j →<br>
i .Agda.Builtin.Equality.≡ j<br>
*-distrib-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverˡ _*_)<br>
_+_<br>
+-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m +
m * n<br>
^-distribˡ-+-*<br>
: (m n p :
ℕ) →<br>
(m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)<br>
distribʳ-*-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
im≡jm+n⇒[i∸j]m≡n<br>
: (i j m n :
ℕ) →<br>
i * m .Agda.Builtin.Equality.≡ j * m + n →<br>
(i ∸ j) * m .Agda.Builtin.Equality.≡ n<br>
isCommutativeSemiring<br>
:
.Algebra.Structures.IsCommutat<wbr>iveSemiring<br>
.Agda.Builtin.Equality._≡_ _+_ _*_ 0 1<br></tt></tt>
<tt>==============================<wbr>=============<br>
<br>
and</tt> <tt><tt>C-c C-z RET _+_ _*_ "distr" RET</tt><br>
will filter definitions which are not about distributivity:<br>
<br></tt>
<tt><tt>==============================<wbr>=============<br></tt></tt>
<tt><tt>Definitions about _+_, _*_, "distr"<br>
*-distrib-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverˡ _*_)<br>
_+_<br>
^-distribˡ-+-*<br>
: (m n p : ℕ) →<br>
(m ^ (n + p)) .Agda.Builtin.Equality.≡ (m
^ n) * (m ^ p)<br>
distribʳ-*-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
==============================<wbr>=============</tt><br>
<br>
This search function respect the normalisation modifiers
(that<br>
is the (C-u)* you can type before most commands) and will
search<br>
types according to the normalisation level you've requested
(and<br>
print results accordingly).<br>
<br>
Cheers,<br>
--<br>
gallais<br>
<br>
<br></tt>
<div>
<div class="m_-9127758530710006032m_-7173118898084949436h5">
<div class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206moz-cite-prefix">On
15/02/18 16:52, Philip Wadler wrote:<br></div>
</div>
</div>
<blockquote type="cite">
<div>
<div class="m_-9127758530710006032m_-7173118898084949436h5">
<div dir="ltr">Is there anything like Hoogle for Agda? It would
save newbies like me a *lot* of time. Cheers, -- P<br>
<div>
<div><br></div>
<div>
<div class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical
Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br></div>
<div>. / \ and Senior Research Fellow, IOHK<br></div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206mimeAttachmentHeader">
</fieldset>
<br></div>
</div>
<pre>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206mimeAttachmentHeader">
</fieldset>
<br>
<pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-9127758530710006032m_-7173118898084949436m_-296081957163068206moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a>
</pre></blockquote>
<br></div>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote>
</div>
<br></div>
The University of Edinburgh is a charitable body, registered
in<br>
Scotland, with registration number SC005336.<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div>
</div>
</blockquote>
</div>
</div>
</div>
</div>
</blockquote>
</div>
<br></div>
The University of Edinburgh is a charitable body, registered in
<br>Scotland, with registration number SC005336.
<br></div></div></span></blockquote></div></div></div></blockquote></div><br></div>