Commit Graph

10023 Commits

Author SHA1 Message Date
Niklas Larsson
c6c928f76c
Merge pull request #4827 from ilyakooo0/lts-15.3
Migrated to lts-15.3
2020-03-20 13:36:59 +01:00
Niklas Larsson
ccbdb4b894
Merge pull request #4830 from melted/fix_ghc_86
Fix build on GHC 8.6
2020-03-19 09:08:51 +01:00
Niklas Larsson
c14f72fd2c Fix build on GHC 8.6 2020-03-18 23:09:34 +01:00
iko
dba5ef4267 Added note 2020-03-19 00:28:19 +03:00
iko
1b614a3e46 Removed broken snapshots 2020-03-19 00:23:31 +03:00
iko
83e4fa5c12 Fixed typo 2020-03-18 21:52:44 +03:00
iko
0380bb9978 Reordered extensions 2020-03-18 21:26:41 +03:00
iko
3fdadd5de5 Updated resolver 2020-03-18 21:24:52 +03:00
iko
b01f45a07a Added stacks 2020-03-18 21:24:08 +03:00
iko
7467a0894e Support megaparsec < 8 2020-03-18 15:44:14 +03:00
Niklas Larsson
87577e31ac
Merge pull request #4829 from alexhumphreys/patch-3
Update introduction.rst with required `-p` flag
2020-03-17 23:47:49 +01:00
Alex Humphreys
289b0589ae
Update introduction.rst
Got the error `Can't find import Effects` when attempting this part of the tutorial. Managed to solve it after finding issue #1524, but would have been faster if this flag was mentioned in the tutorial.
2020-03-17 15:09:45 +01:00
Niklas Larsson
93cfe987f3
Merge pull request #4820 from nickdrozd/reverse
More proofs, simpler proofs
2020-03-14 01:58:14 +01:00
iko
49d7b89a96 Removed GHC 8.6 2020-03-13 17:34:51 +03:00
iko
71d139087b wip 2020-03-13 17:05:17 +03:00
iko
68efb0ac4d wip 2020-03-13 16:22:54 +03:00
iko
d60d56f7ca Try using LD_PRELOAD 2020-03-13 15:57:03 +03:00
iko
ba1c1b5f7e Temporarily removed caches 2020-03-13 13:24:08 +03:00
iko
912ac9319c Added libffi addon 2020-03-13 00:27:03 +03:00
iko
ad91f0396f Removed ghc 8.4 2020-03-12 23:09:15 +03:00
iko
c80e65f84d Fixed stylish-haskell build error 2020-03-12 22:42:48 +03:00
iko
73937215dc Removed stack-alt.yaml from Extra-source-files 2020-03-12 22:40:08 +03:00
iko
0c81cf8295 Updated travis 2020-03-12 22:19:10 +03:00
iko
d7a669bf95 Migrated to lts-15.3 2020-03-12 22:04:17 +03:00
Jan de Muijnck-Hughes
853e4533e7
Merge pull request #4825 from jfdm/doc-fixes
Fix Readthedocs PDF generation
2020-03-10 14:47:40 +00:00
Jan de Muijnck-Hughes
c76ade1f0a Fix Readthedocs PDF generation
RTD is consistently not building the PDF of the Idris Documentation. I think it is because we have two documents built.
I have made the opinion to only have the main tutorial build, as this would be of most interest to others.
2020-03-10 14:45:05 +00:00
Jan de Muijnck-Hughes
b7a191bbf3
Merge pull request #4823 from jfdm/doc-fixes
Minor fix to latex sphinx build configuration.
2020-03-10 14:20:32 +00:00
Jan de Muijnck-Hughes
bc8926c1b9 Minor fix to latex sphinx build configuration.
Build was failing locally with \textlambda not being found. Added new package for fix.

Changed name of generated pdf to match project name, and removed second PDF file in list. This hopefuly will make RTD build again...

Update PDF of tutorial in source repository.
2020-03-10 14:17:53 +00:00
Nick Drozd
8684daec51 Align steps in preorder reasoning example 2020-03-06 16:07:00 -06:00
Nick Drozd
588bc99229 Simplify isomorphism proofs 2020-03-06 16:07:00 -06:00
Nick Drozd
76c37e765c Simplify proofs of algebra laws 2020-03-06 16:07:00 -06:00
Nick Drozd
1f56ca89e3 Further simplify Nat proofs 2020-03-06 16:07:00 -06:00
Nick Drozd
ec395a7a29 Add more reverse properties 2020-03-06 16:07:00 -06:00
Nick Drozd
2e994cdef1 Rename List.Extra to List.Reverse 2020-03-06 16:07:00 -06:00
Edwin Brady
bbd0f286c2 Fix fileModifiedTime on 32 bit systems
Can't use MKBIGI for the result, since that'll be a negative number for
the current time! So use MKBIGUI instead to ensure it stays unsigned.
2020-03-06 09:13:00 +00:00
Niklas Larsson
10fd4e71f8
Merge pull request #4812 from nickdrozd/factorial
Add factorial proofs
2020-02-29 14:19:31 +01:00
Niklas Larsson
3d83aa0345
Merge pull request #4818 from nickdrozd/proofs
Simplify some Nat proofs
2020-02-29 14:19:08 +01:00
Nick Drozd
1653d3ead0 Simplify parity arithmetic proofs 2020-02-28 17:35:59 -06:00
Nick Drozd
b72dfc98b4 Add more parity proofs and some commentary 2020-02-28 17:25:17 -06:00
Nick Drozd
7ecd2ff576 Simplify some Nat proofs 2020-02-25 19:29:16 -06:00
Nick Drozd
f80809a157 Add factorial proofs 2020-02-03 21:45:55 -06:00
Niklas Larsson
10b7fe8bca
Mention Idris 2 in README 2020-02-01 01:18:52 +01:00
Niklas Larsson
fc0acd9f00
Merge pull request #4805 from martinbaker/parseLibDoc2
Extend and Fix Parser Library Documentation
2020-02-01 01:12:19 +01:00
Niklas Larsson
9074a76cb3
Merge pull request #4806 from mokshasoft/rts-stdfgn
Rts stdfgn
2020-02-01 01:11:34 +01:00
Niklas Larsson
70ebef5f0e
Merge pull request #4810 from wstrm/docs-num-lines-js
Change lines of code of JavaScript to 60 for Hello World example in docs
2020-02-01 01:10:37 +01:00
Niklas Larsson
246c890f89
Merge pull request #4811 from melted/idris2-travis
Add a travis target building Idris 2
2020-02-01 01:09:37 +01:00
Niklas Larsson
bc5ee4b189 Add a travis target building Idris 2 2020-01-31 22:51:56 +01:00
William Wennerström
55df0fb894
Change lines of code of JavaScript to 60 for Hello World example in docs
A simple hello world program now produces about 60 lines of code:
```
~/projects/learn-idris ξ cat hello.idr
main : IO ()
main = putStrLn "Hello, world!"
~/projects/learn-idris ξ idris --codegen javascript hello.idr -o hello.js
~/projects/learn-idris ξ wc -l hello.js
61 hello.js
```

Far from 1500! Hooray :)
2020-01-27 18:58:10 +01:00
Niklas Larsson
53f6fc98b1
Merge pull request #4808 from melted/ghc-8.8
Compile with GHC 8.8
2020-01-25 19:35:39 +01:00
Niklas Larsson
9662ab5e4a Disable travis for GHC 8.8 (libffi still broken)
Update changelog

Use GHC 8.8 in Appveyor

Run legacy test commands
2020-01-25 18:48:50 +01:00