Merge pull request #564 from ska80/post-idris2boot-cleanups

More post-Idris2-boot cleanups

INSTALL.md

@@ -44,9 +44,8 @@ Make sure that:
 
 ### 2: Installing without an existing Idris 2
 
-If you _don't_ have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot) installed, you can build from pre-built
+You can build from pre-built Chez Scheme source, as long as you have Chez Scheme
-Chez Scheme source, as long as you have Chez Scheme installed (or,
+installed (or, alternatively, Racket). To do this, enter one of the following:
-alternatively, Racket). To do this, enter one of the following:
 
 - `make bootstrap SCHEME=chez`
 - `make bootstrap-racket`
@@ -65,20 +64,14 @@ If all is well, to install, type:
 
 - `make install`
 
-### (Alternative 2: Installing with an existing Idris 2)
+### 3: Installing with an existing Idris 2
 
-If you have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot)
+If you have an earlier version of this Idris 2 installed
-installed:
-
-- `make all IDRIS2_BOOT=idris2boot`
-- `make install IDRIS2_BOOT=idris2boot`
-
-If you have an earlier version of this Idris 2 installer
 
 - `make all`
 - `make install`
 
-### 3: (Optional) Self-hosting step
+### 4: (Optional) Self-hosting step
 
 As a final step, you can rebuild from the newly installed Idris 2 to verify
 that everything has worked correctly. Assuming that `idris2` is in your
@@ -87,12 +80,12 @@ that everything has worked correctly. Assuming that `idris2` is in your
 - `make clean` -- to make sure you're building everything with the new version
 - `make all && make install`
 
-### 4: Running tests
+### 5: Running tests
 
 After `make all`, type `make test` to check everything works. This uses the
 executable in `./build/exec`.
 
-### 5: (Optional) Installing the Idris 2 API
+### 6: (Optional) Installing the Idris 2 API
 
 You'll only need this if you're developing support tools, such as an external
 code generator. To do so, once everything is successfully installed, type:

src/TTImp/Interactive/ExprSearch.idr

@@ -35,7 +35,6 @@ import Data.List
 
 -- Data for building recursive calls - the function name, and the structure
 -- of the LHS. Only recursive calls with a different structure are okay.
-public export -- to keep Idris2-boot happy!
 record RecData where
   constructor MkRecData
   {vars : List Name}
@@ -592,7 +591,7 @@ makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
          -- Go right to left on variable split, to get the variable we just
          -- added first.
          -- There must be at least one case split.
-         ((helper :: _), nextdef) <- 
+         ((helper :: _), nextdef) <-
                     searchN 1 $ gendef (record { getRecData = False,
                                                  inUnwrap = True,
                                                  depth = depth',
@@ -601,14 +600,14 @@ makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
                                        helpern 0 ty
               | _ => do log 10 "No results"
                         noResult
-         
+
          let helperdef = IDef fc helpern (snd helper)
          log 10 $ "Def: " ++ show helperdef
          pure (Result (def, helperdef :: ds) -- plus helper
                       (do next' <- next
                           makeHelper fc rig opts env letty targetty next'))
   where
-    -- convert a metavar application (as created by 'metaVar') to a normal 
+    -- convert a metavar application (as created by 'metaVar') to a normal
     -- application (as required by a case block)
     toApp : forall vars . Term vars -> Term vars
     toApp (Meta fc n i args) = apply fc (Ref fc Func (Resolved i)) args
@@ -645,8 +644,8 @@ tryIntermediateWith fc rig opts env ((p, pty) :: rest) ty topty
           -- something we can pattern match on (so, NTCon) then apply it,
           -- let bind the result, and try to generate a definition for
           -- the scope of the let binding
-          do True <- matchable defs 
+          do True <- matchable defs
-                           !(sc defs (toClosure defaultOpts env 
+                           !(sc defs (toClosure defaultOpts env
                                                 (Erased fc False)))
                  | False => noResult
              intnty <- genVarName "cty"
@@ -680,7 +679,7 @@ tryIntermediateRec : {vars : _} ->
                      {auto m : Ref MD Metadata} ->
                      {auto u : Ref UST UState} ->
                      FC -> RigCount -> SearchOpts ->
-                     Env Term vars -> 
+                     Env Term vars ->
                      Term vars -> ClosedTerm ->
                      Maybe RecData -> Core (Search (Term vars, ExprDefs))
 tryIntermediateRec fc rig opts env ty topty Nothing = noResult
@@ -754,7 +753,7 @@ searchType fc rig opts env topty _ ty
                                    case recData opts of
                                         Nothing => []
                                         Just rd => [tryRecursive fc rig opts env ty topty rd]
-                             let tryIntRec = 
+                             let tryIntRec =
                                    if doneSplit opts
                                       then [tryIntermediateRec fc rig opts env ty topty (recData opts)]
                                       else []

tests/Main.idr

@@ -245,10 +245,7 @@ runTest opts testPath
                      | Left err => do print err
                                       pure False
                  let result = normalize out == normalize exp
-                 -- The issue #116 that made this necessary is fixed, but
+                 if result
-                 -- please resist putting 'result' here until it's also
-                 -- fixed in Idris2-boot!
-                 if normalize out == normalize exp
                     then putStrLn "success"
                     else do
                       putStrLn "FAILURE"