Merge pull request #1599 from edwinb/prepare-040

edwinb · web-flow · commit ea1ad1688f1e · 2021-06-23T19:37:12.000+01:00
Changes for next release, 0.4.0
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,6 @@
 # Changelog
 
-## Unreleased (idris2-next)
+## v0.4.0
 
 ### Syntax changes
 
@@ -52,6 +52,9 @@
 * Added `:search` command, which searches for functions by type
 * `:load`/`:l` and `:cd` commands now only accept paths surrounded by double
   quotes
+* Added a timeout to "generate definition" and "proof search" commands,
+  defaulting to 1 second (1000 milliseconds) and configurable with
+  `%search_timeout <time in milliseconds>`
 
 ### Library Changes
 
@@ -165,6 +168,9 @@ Added
 
 ### Other changes
 
+* Lots of small performance improvements, some of which may be especially
+  noticeable in programs that do a lot of type level evaluation.
+* Added HTML documentation generation, using the `--mkdoc` flag
 * Support for auto-completion in bash-like shells was added.
 * Fixed case-splitting to respect any indentation there may be in the term being
   case-split and the surrounding symbols, instead of filtering out the
diff --git a/Makefile b/Makefile
@@ -9,7 +9,7 @@ TARGETDIR = ${CURDIR}/build/exec
 TARGET = ${TARGETDIR}/${NAME}
 
 MAJOR=0
-MINOR=3
+MINOR=4
 PATCH=0
 
 GIT_SHA1=
diff --git a/Release/CHECKLIST b/Release/CHECKLIST
@@ -1,6 +1,9 @@
 [ ] Change version number (MAJOR, MINOR, PATCH) in Makefile
 [ ] Change version numbers in doc listings
 [ ] Change version numbers in prelude, base, contrib, network, and test ipkgs
+[ ] Change version number in idris2api.ipkg
+[ ] Change version number in flake.nix
+[ ] Change version number in test pkg010 (TODO: make this step unnecessary!)
 [ ] Update bootstrap chez and racket
 [ ] Tag on github with version number (in the form vX.Y.Z)
 [ ] make libdocs and upload to idris-lang.org
diff --git a/bootstrap/idris2_app/idris2.rkt b/bootstrap/idris2_app/idris2.rkt
diff --git a/bootstrap/idris2_app/idris2.ss b/bootstrap/idris2_app/idris2.ss
diff --git a/docs/source/listing/idris-prompt-helloworld.txt b/docs/source/listing/idris-prompt-helloworld.txt
@@ -1,7 +1,7 @@
 $ idris2 hello.idr
      ____    __     _         ___
     /  _/___/ /____(_)____   |__ \
-    / // __  / ___/ / ___/   __/ /     Version 0.3.0
+    / // __  / ___/ / ___/   __/ /     Version 0.4.0
   _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
  /___/\__,_/_/  /_/____/   /____/      Type :? for help
 
diff --git a/docs/source/listing/idris-prompt-interp.txt b/docs/source/listing/idris-prompt-interp.txt
@@ -1,7 +1,7 @@
 $ idris2 interp.idr
      ____    __     _         ___
     /  _/___/ /____(_)____   |__ \
-    / // __  / ___/ / ___/   __/ /     Version 0.3.0
+    / // __  / ___/ / ___/   __/ /     Version 0.4.0
   _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
  /___/\__,_/_/  /_/____/   /____/      Type :? for help
 
diff --git a/docs/source/listing/idris-prompt-start.txt b/docs/source/listing/idris-prompt-start.txt
@@ -1,7 +1,7 @@
 $ idris2
      ____    __     _         ___
     /  _/___/ /____(_)____   |__ \
-    / // __  / ___/ / ___/   __/ /     Version 0.3.0
+    / // __  / ___/ / ___/   __/ /     Version 0.4.0
   _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
  /___/\__,_/_/  /_/____/   /____/      Type :? for help
 
diff --git a/docs/source/reference/packages.rst b/docs/source/reference/packages.rst
@@ -130,6 +130,9 @@ Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler
 
 + ``idris2 --clean test.ipkg`` will clean the intermediate build files.
 
++ ``idris2 --mkdoc test.ipkg`` will generate HTML documentation for the
+  package, output to ``build/docs``
+
 Once the test package has been installed, the command line option
 ``--package test`` makes it accessible (abbreviated to ``-p test``).
 For example::
diff --git a/flake.nix b/flake.nix
@@ -8,7 +8,7 @@
   };
 
   outputs = { self, nixpkgs, flake-utils, idris-emacs-src }:
-    let idris2-version = "0.3.0";
+    let idris2-version = "0.4.0";
     in flake-utils.lib.eachDefaultSystem (system:
       let pkgs = import nixpkgs { inherit system; };
           idris2Pkg = pkgs.callPackage ./nix/package.nix { inherit idris2-version; };
diff --git a/idris2api.ipkg b/idris2api.ipkg
@@ -1,5 +1,5 @@
 package idris2
-version = 0.3.0
+version = 0.4.0
 
 modules =
     Algebra,
diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr
@@ -34,8 +34,10 @@ prim__newBuffer : Int -> PrimIO Buffer
 export
 newBuffer : HasIO io => Int -> io (Maybe Buffer)
 newBuffer size
-    = do buf <- primIO (prim__newBuffer size)
-         pure $ Just buf
+    = if size >= 0
+            then do buf <- primIO (prim__newBuffer size)
+                    pure $ Just buf
+                 else pure Nothing
 --          if prim__nullAnyPtr buf /= 0
 --             then pure Nothing
 --             else pure $ Just $ MkBuffer buf size 0
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
@@ -1,5 +1,5 @@
 package base
-version = 0.3.0
+version = 0.4.0
 
 opts = "--ignore-missing-ipkg -Wno-shadowing"
 
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
@@ -1,5 +1,5 @@
 package contrib
-version = 0.3.0
+version = 0.4.0
 
 opts = "--ignore-missing-ipkg -Wno-shadowing"
 
diff --git a/libs/network/network.ipkg b/libs/network/network.ipkg
@@ -1,5 +1,5 @@
 package network
-version = 0.3.0
+version = 0.4.0
 
 opts = "--ignore-missing-ipkg -p contrib"
 
diff --git a/libs/prelude/prelude.ipkg b/libs/prelude/prelude.ipkg
@@ -1,5 +1,5 @@
 package prelude
-version = 0.3.0
+version = 0.4.0
 
 opts = "--ignore-missing-ipkg --no-prelude"
 
diff --git a/libs/test/test.ipkg b/libs/test/test.ipkg
@@ -1,5 +1,5 @@
 package test
-version = 0.3.0
+version = 0.4.0
 
 depends = contrib
 
diff --git a/src/Libraries/Utils/Binary.idr b/src/Libraries/Utils/Binary.idr
@@ -222,6 +222,7 @@ TTC String where
   fromBuf b
       = do len <- fromBuf {a = Int} b
            chunk <- get Bin
+           when (len < 0) $ corrupt "String"
            if toRead chunk >= len
               then
                 do val <- coreLift $ getString (buf chunk) (loc chunk) len
@@ -252,7 +253,7 @@ TTC Binary where
          if toRead chunk >= len
             then
               do Just newbuf <- coreLift $ newBuffer len
-                      | Nothing => throw (InternalError "Can't create buffer")
+                      | Nothing => corrupt "Binary"
                  coreLift $ copyData (buf chunk) (loc chunk) len
                                      newbuf 0
                  put Bin (incLoc len chunk)
diff --git a/tests/Main.idr b/tests/Main.idr
@@ -123,7 +123,8 @@ idrisTestsRegression = MkTestPool "Various regressions" [] Nothing
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
        "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
-       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042"]
+       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042",
+       "reg043"]
 
 idrisTestsData : TestPool
 idrisTestsData = MkTestPool "Data and record types" [] Nothing
diff --git a/tests/idris2/pkg010/expected.in b/tests/idris2/pkg010/expected.in
@@ -1,3 +1,3 @@
 1/1: Building Main (Main.idr)
-Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.3.0/testpkg-0
-Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.3.0/testpkg-0
+Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
+Installing __PWD__build/ttc/Main.ttc to __PWD__currently/nonexistent/dir/idris2-0.4.0/testpkg-0
diff --git a/tests/idris2/reg043/TestFake.idr b/tests/idris2/reg043/TestFake.idr
@@ -0,0 +1 @@
+import Fake
diff --git a/tests/idris2/reg043/expected b/tests/idris2/reg043/expected
@@ -0,0 +1,2 @@
+1/1: Building TestFake (TestFake.idr)
+Error: Error in TTC file: Corrupt TTC data for String (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files)
diff --git a/tests/idris2/reg043/run b/tests/idris2/reg043/run
@@ -0,0 +1,6 @@
+mkdir -p build/ttc
+echo "TT2This Is A Fake TTC" > build/ttc/Fake.ttc
+
+$1 --no-color --console-width 0 --check TestFake.idr
+
+rm -rf build

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+1/1: Building TestFake (TestFake.idr)`
	`2`	`+Error: Error in TTC file: Corrupt TTC data for String (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files)`