Commit Graph

10023 Commits

Author SHA1 Message Date
Jan de Muijnck-Hughes
99ac2025ca
Merge pull request #4718 from martinbaker/interactiveDocFix
fix formatting error which caused missing code block
2019-05-29 12:28:13 +01:00
Jan de Muijnck-Hughes
aed33b861b
Merge pull request #4719 from klangner/master
Added examples to the Vect doc
2019-05-29 12:27:19 +01:00
klangner
cc30a89f47 Added examples to the Vect doc 2019-05-27 13:59:16 +02:00
Martin Baker
0ccc003086 fix formatting error which caused missing code block 2019-05-24 17:18:05 +01:00
Martin Baker
19d6e296c2 tidy up diagrams for example 2019-05-23 11:53:47 +01:00
Niklas Larsson
ef51a46e15
Merge pull request #4705 from nickdrozd/reverse-proofs
Simplify reverse proofs
2019-05-23 10:11:40 +02:00
Martin Baker
75feef7e0b fix example code for generating functions 2019-05-23 08:17:37 +01:00
Martin Baker
b093a14c56 add diagram to illustrate Raw structure used for function definition 2019-05-22 17:00:47 +01:00
Martin Baker
671bb4d633 changes to primitive.rst 2019-05-22 08:55:45 +01:00
Martin Baker
543a382a0f changes to tactics.rst 2019-05-22 08:47:53 +01:00
Martin Baker
1b71663573 changes to tactics.rst 2019-05-22 08:19:39 +01:00
Martin Baker
ff054c14ec changes to generatingData.rst 2019-05-22 08:00:09 +01:00
Martin Baker
231d842304 changes to generatingData.rst 2019-05-21 17:36:58 +01:00
Martin Baker
08c0900d62 changes to generatingData.rst 2019-05-21 17:05:06 +01:00
Martin Baker
566daf7f71 changes to generatingData.rst 2019-05-20 19:04:41 +01:00
Martin Baker
6255c0d1c0 add svg diagram 2019-05-19 17:42:46 +01:00
Martin Baker
d85b8c6e5a more small changes 2019-05-19 17:07:15 +01:00
Martin Baker
a13f2ab452 more small changes 2019-05-19 11:30:28 +01:00
Martin Baker
73dfb0c005 update some diagrams for example 2019-05-18 16:01:50 +01:00
Martin Baker
540e76bb89 remove some duplicated definitions and tidy up 2019-05-18 11:39:18 +01:00
Martin Baker
654c43178b rename file 2019-05-18 09:17:02 +01:00
Martin Baker
edd8da70ba start to make changes to identity example 2019-05-17 18:57:46 +01:00
Martin Baker
efbb287661 change text around logic diagram 2019-05-17 17:46:18 +01:00
Martin Baker
893350512b remove space which caused incorrect formatting 2019-05-17 17:26:19 +01:00
Martin Baker
7b70c6c3b8 improve some diagrams 2019-05-17 17:02:28 +01:00
Martin Baker
dd2c427533 update elabOverview image 2019-05-16 19:09:51 +01:00
Martin Baker
40c7a8a542 update copyright notice to 2019 2019-05-16 15:03:23 +01:00
Jan de Muijnck-Hughes
2418112a2e
Merge pull request #4709 from jfdm/new-stack
Stack 'fixes'
2019-05-16 11:15:58 +01:00
Jan de Muijnck-Hughes
4efeda8867
Merge pull request #4708 from jfdm/show-visibility-in-docs
Show visibility in doc comments.
2019-05-16 11:14:58 +01:00
Jan de Muijnck-Hughes
dbf060cf17 Updated changelog and add GitHub issue reference: Fixes #4702 2019-05-16 11:14:21 +01:00
Jan de Muijnck-Hughes
f25bcfe30f Add an alternative stack configuration file to deal with upstream GHC issues.
There is an upstream issue with GHC on some Ubuntu and Fedora machines.
The issue is that for GHC versions greater than 8.4.X linking to libFFI is broken.
See the following GHC issue page for more information:

  <https://gitlab.haskell.org/ghc/ghc/issues/15397>

This means that an Idris built with `libFFI` support will fail at runtime as the executable would not be able to find the correct `libffi` shared object.
This will cause the build to fail.

This commit adds an alternative stack configuration file to help bypass the issues for those affected by the issue.
2019-05-16 11:10:19 +01:00
Jan de Muijnck-Hughes
e09ab811b4 Bump stack to latest version. 2019-05-16 11:01:03 +01:00
Martin Baker
ae9484a316 more suggested changes 2019-05-16 08:25:38 +01:00
Martin Baker
5cd37d80c1 change as suggested 2019-05-15 18:46:35 +01:00
Martin Baker
5267e39a84 fix reference 2019-05-15 18:36:06 +01:00
Martin Baker
0fb8b7504b fix typo 2019-05-15 18:19:49 +01:00
Martin Baker
420f2b8d90 add readme file to explain image file formats 2019-05-15 18:16:06 +01:00
Martin Baker
d0a4575912 further improvements from comments 2019-05-15 17:43:26 +01:00
Jan de Muijnck-Hughes
8fe28aa163 Amended the test suite to report updated documentation. 2019-05-15 13:47:41 +01:00
Martin Baker
9472245345 inital changes following comments, more to come 2019-05-15 11:13:33 +01:00
Jan de Muijnck-Hughes
36bcf4b5a8 Show visibility in doc comments.
Currently the result of `:doc` displays totality information for functions.
However there are two scenarios where having the accessiblity/visibility information would be beneficial:

1. Type-level computations failing to reduce.

A computed value in your type might fail to reduce in the definition of the computing function is not public c.f. exportation of functions computing type synonyms.
A good numpty check would be to add this information to the doc output, much as we do for totality status.

2. Working with 'Exported' constructors.

Much like exported functions, some data types might be exported rather than public exported.
One has to assert the functions visibility by checking the source code, this is cumbersome.

This commit adds visibility status to the documentation output.
Such that if totality information is to be displayed we output the totality and accessibility information, otherwise we just output the accessibility information.
2019-05-15 09:20:14 +01:00
Nick Drozd
3b8c83a58f Simplify reverse proofs 2019-05-13 18:16:21 -05:00
Niklas Larsson
c8f7604864
Merge pull request #4701 from melted/time_win
Implement idris_clock on windows
2019-05-09 08:11:26 +02:00
Martin Baker
1772239d54 minor change - add reference 2019-05-09 07:07:51 +01:00
Niklas Larsson
7626280473 Implement idris_clock on windows 2019-05-09 01:28:59 +02:00
Martin
5eebc7b046 Replace &gt; with > in definitional.rst 2019-05-08 20:45:53 +02:00
Jelle Besseling
19a87f3064 Remove space before full stop 2019-05-08 20:45:04 +02:00
Martin Baker
5e25d2b5b4 fix minor formatting issue 2019-05-08 18:53:37 +01:00
Martin Baker
278de0611f change title of theorem proving section 2019-05-08 16:56:07 +01:00
Martin Baker
b6fde49227 fix image paths 2019-05-08 16:44:47 +01:00