Commit Graph

3080 Commits

Author SHA1 Message Date
Gregory Werbin
b81f5280c1 Use consistent punctuation & indentation 2022-11-11 09:33:09 +01:00
Gregory Werbin
ecac93081b Add CPPFLAGS for consistency? 2022-11-11 09:33:09 +01:00
Gregory Werbin
c5c842726a Add support for standard C env vars
Also, organize the env var listing a bit more.
2022-11-11 09:33:09 +01:00
Gregory Werbin
1020437aad Use CPPFLAGS when needed 2022-11-11 09:33:09 +01:00
Mathew Polzin
25388ecac2 look for lib folders in package directories. 2022-11-04 18:10:03 -05:00
Guillaume Allais
8556c81014 [ new ] typed ABT 2022-11-04 16:20:46 +00:00
Thomas E. Hansen
dc1662ddf1 [ doc ] Add :doc for unquotes
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2022-11-04 14:03:21 +00:00
G. Allais
fd46e31da3
[ new ] typed Krivine (#2749) 2022-11-04 10:05:31 +00:00
Stefan Höck
b5decdf729
[ new ] add --ttc-version command (#2752)
* [ new ] add --ttc-version command

* [ fix ] -v should still print version
2022-11-04 06:45:49 +00:00
stefan-hoeck
6f5b19c389 [ cleanup ] bifoldMap already in Prelude 2022-11-03 14:11:15 +00:00
Andy Lok
ddcbe795c6
[ fix ] DISallow grouping pi with different types (#2680)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-11-02 14:33:19 +00:00
G. Allais
ad817538e0
[ new ] typed SECD (#2743) 2022-11-02 12:58:13 +00:00
Stefan Höck
9c9ffe4a31
[ fix ] isue 2745 (#2747)
* [ fix ] .ipkg install dir

* [ test ] .ipkg install dir

* [ doc ] update CHECKLIST

* [ doc ] add explanation to pkg016 test

* [ cleanup ] no need to clutter CHECKLIST
2022-11-02 12:01:19 +00:00
G. Allais
4cd38a8c5d
[ new ] deriving Show (#2741) 2022-11-02 11:57:07 +00:00
Zoe Stafford
078445b178
Merge pull request #2744 from dunhamsteve/bang-fc
[ parser ] Better error messages for type mismatch on bang expressions
2022-11-02 07:06:11 +00:00
Steve Dunham
3c0eadee07 [ parser ] Better error messages for type mismatch on bang expressions 2022-11-01 20:18:33 -07:00
G. Allais
19d0cbcd37
[ new ] put TTC files in a version-tagged directory (#2684) 2022-11-01 18:11:18 +00:00
G. Allais
ee8113bb9d
[ papers ] A Completely Unique Account of Enumeration (#2659) 2022-11-01 16:31:57 +00:00
Steve Dunham
c2bcc14e00 [ doc ] Fix broken links from README to wiki 2022-10-29 10:16:42 +01:00
Nathan McCarty
407409fecc
[ ci ] Simplify bootstrap process in nix (#2731) 2022-10-28 19:29:30 +01:00
Stefan Höck
85ddafbac5
[ fix ] bump version of linear and papers packages (#2735) 2022-10-28 08:55:35 +01:00
Edwin Brady
102d7ebc18
Update version number in CHANGELOG (#2734) 2022-10-27 16:41:13 +01:00
Edwin Brady
e125c9014f
Prepare release 0.6.0 (#2733)
* Prepare release 0.6.0

* Fix bootstrap chez

* Correct version in bootstrap chez
2022-10-27 16:32:16 +01:00
Stefan Höck
57c589ca80
[ performance ] More stack safety in the Prelude (#2704) 2022-10-26 09:54:53 +01:00
Steve Dunham
b1f2eab6d6 Update nix build scripts to build idris with the current version of idris 2022-10-25 14:52:45 +01:00
Aleksei Volkov
c906720ee3
[ base ] Change Reader to fix search for MonadReader instance (#2729) 2022-10-22 19:13:52 +01:00
Guillaume Allais
542ebeae97 [ fix 2726 ] more peeling of Erased 2022-10-22 10:07:39 +01:00
Guillaume Allais
86bd19b64d [ fix ] add missing recursive calls 2022-10-22 10:07:39 +01:00
Guillaume Allais
3f7cd84ccb [ cleanup ] traversable instances 2022-10-22 10:07:39 +01:00
Guillaume Allais
3dd8b9cc3c tmp 2022-10-22 10:07:39 +01:00
G. Allais
475d13bb11
[ fix ] parsing of test lib's options (#2725)
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2022-10-21 21:01:54 +01:00
CodingCellist
59460c2f46
[ admin ] Update CHANGELOG and CONTRIBUTORS (#2703)
* [ admin ] Update CHANGELOG and CONTRIBUTORS

We really need to do a release at some point...

* [ ci ] Don't check capitalised proper names in links and code

Sometimes hyperlinks and code-blocks just don't use the "proper"
capitalisation (e.g. `.html` vs `.HTML`), and that's okay.
(or even critical as links may not be found without "incorrect" format)

* [ ci ] Don't check terminology in links and code-blocks

Hopefully this is the right fix for the problem in #2703

* [ ci ] 3rd attempt at fixing nl linter

* [ ci ] Attempt no. 4 at fixing nl linter

* [ ci ] Point NL linter at YAML config file

Was that actually it??

* Update CHANGELOG.md

* Add note about forward declaration of records

* [ admin ] Add PR template with CHANGELOG reminder

To hopefully help mitigate big crawl-throughs of what's changed,
à la #2703.

* [ admin ] Reflow CHANGELOG to 80 characters where possible

Only done for the "next version" changes for the sake of diff size.
(Personally, I'd want to have the linter enforce this, but that might be
too extreme; there's already a note in the CI config complaining about
line length...)

* [ admin ] Make linter happy

It never ends...

Co-authored-by: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Co-authored-by: Steve Dunham <dunhamsteve@gmail.com>
2022-10-21 16:48:37 +02:00
CodingCellist
47c2de3148
[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)
A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.

Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.

This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.

* [ repl ] Use unlines for detailed help (see #2087)

  Ideally, the lines affected should be multiline strings. But for some
  arcane reason, newlines in those get swallowed in Nix and Windows
  **CI** only Ô.o
  This was already documented in issue #2087.

* [ new ] --except for golden testing lib

  To allow CI to pass despite #2087

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-21 14:35:33 +02:00
Guillaume Allais
a39783be8e [ fix #2721 ] Don't reflow doc lines
I don't think there's a good solution at least until we start
parsing these comments so let's just keep them as they were written
by the library writer.
2022-10-19 09:09:11 +01:00
André Videla
fce45c5762
Merge pull request #2717 from MithicSpirit/main
Reduce ambiguity in dependent types `filter` example
2022-10-18 14:16:17 +01:00
QDelta
e0a19aa01e
[ fix #2719 ] --only behavior in Test.Golden (#2720)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-10-18 12:36:09 +01:00
tangcl
0b1874e4fd Change notId's definition 2022-10-16 20:34:50 +01:00
MithicSpirit
acd9c09a05
Reduce ambiguity in dependent types filter example
`p` was used for both the filter predicate and the length of the
filtered vector. This renames the latter to n'.
2022-10-16 00:44:54 -04:00
Zoe Stafford
bc8b6bb7a7
Merge pull request #2715 from Z-snails/parser-fc
[ parser ] fix FC for type declarations
2022-10-14 21:30:07 +01:00
Zoe Stafford
c2e4773ed7 [ parser ] fix FC for type declarations 2022-10-14 18:56:28 +01:00
G. Allais
51d00638b0
[ cosmetic ] Say when you start compiling the executable (#2714) 2022-10-14 16:21:19 +01:00
G. Allais
30866fa892
[ new ] do not split on dotted patterns (#2706) 2022-10-14 16:21:06 +01:00
Denis Buzdalov
eb4cc0054b [ golden ] Make options to store more flexible tests filter 2022-10-14 15:03:05 +01:00
Steve Dunham
b15be4a70a [ new ] Allow forward declarations of records 2022-10-14 14:58:29 +01:00
CodingCellist
bb602643b1
[ fix #2712 ] Don't consider CyclicMeta recoverable (#2713) 2022-10-14 14:57:55 +01:00
Thomas E. Hansen
6823915dd0 [ tests ] Check REPL help text and module import cmds
The help text check is for making sure we update it when modifying
things, more than anything else.
2022-10-13 11:31:05 +02:00
Thomas E. Hansen
a598fec4f7 [ repl ] Add :import command 2022-10-13 11:31:05 +02:00
Denis Buzdalov
3ca065b85d [ fix #2088 ] Make %runElab expression propagate its rig to check 2022-10-07 10:55:22 +02:00
Denis Buzdalov
2744a3a5a2
[ golden ] Truncate long test names when printing the results (#2553) 2022-10-06 19:18:34 +01:00
Zoe Stafford
c69f439c2d
[ cleanup ] Compiler/* modules (#2694)
* cleanup(Compiler/*)
cleanup some messy/unclear code
Also use primitives directly where possible, instead of idris's wrappers

* Fix tests
2022-10-06 10:17:38 +02:00