Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

Implement pragma for declaring nat optimizations

Open fabianhjr opened this issue 5 years ago • 4 comments

fabianhjr avatar May 03 '20 03:05 fabianhjr

Helped me improve the performance of an alternative idris2 prelude I am playing with, tested with mock of ProjectEuler problem #1:

module NaiveSolution

import Prelude

import Data.Integral
import Data.Nat.Integral

main : LinkedList Nat
main = filter (`divBy` (the Nat 3)) [(the Nat 1)..100]

fabianhjr avatar May 03 '20 05:05 fabianhjr

Marceline discovered that this PR causes an explosion of memory usage while compiling Idris2 in Core/Binary (Extra ~ 5GB or so of memory usage)

fabianhjr avatar May 03 '20 07:05 fabianhjr

This does make the nat hack a bit less hacky, thanks! Is the compile time performance still an issue? Sometimes that can be due to ambiguity resolution going a bit out of control.

edwinb avatar May 09 '20 12:05 edwinb

Yes, there is still an issue with Idris1 compilation of Idris2.

Idris2 runs fine though.

fabianhjr avatar May 09 '20 16:05 fabianhjr