Stefan Höck
Stefan Höck
How about: ```idris doubleWithCornerCases : Gen Double doubleWithCornerCases = frequency [ (4, double $ linearFracFrom 0 (-999) 999) , (1, element [-1 / 0, 1 / 0, 0 / 0])...
I think the most simple option in this case would be to add a (hidden) file containing the commit of the compiler used to build a local package to its...
> * If there is no file containing the commit, should the code be rebuilt with cleaning? For consistency, it definitely should, but it means that interleaving `pack` and direct...
As a second thought, I wonder whether `idris2 --clean` should actually completely remove the `build` dir?
Am I right in assuming that this will no longer be needed once idris-lang/Idris2#2684 lands? Otherwise I got a fix ready where pack will add an `.idrisVersion` file to the...
So, I have merged a simple fix for this. Simple enough that it can be easily undone should we no longer need it.
Sorry for the late response. This would surely be a nice thing to have, but it will require some planning - so of which you have already done above -...
This is indeed a caching issue: Currently, in order to decide if a local package needs to be reinstalled, pack only checks the timestamps of all files in the source...
Sorry for the late reply. Obviously, I'm not a Windows users, so I won't myself be able to test / maintain Windows support. This means that if Windows support breaks...
This is a good idea and would be a nice thing to have. Contributions welcome.