Skip to content

Library incompatible with recent Idris versions #4

@lambdacasserole

Description

@lambdacasserole

First of all, great library! We're putting it to use at the Software Reliability Lab in some Idris projects we have going that focus on dependent types for reliable software. We had to make some changes to get it working with the latest version of Idris (v1.3.1), however. Briefly, these were:

  • The Float type had a name change to Double a while back.
  • The call to pow in Display.idr became ambiguous as pow was added to another namespace. This is fixed by fully qualifying the name.
  • The return alias became deprecated, so it has been changed to pure.
  • A number of syntax changes and tweaks brought across from PR update for idris 1.0 #1, originally opened by @clayrat.

A few CI-related issues have also been addressed:

  • The installation of Idris via cabal was timing out. This has been fixed by wrapping the command in travis_wait.
  • After installing Idris via cabal, it's no longer added/symlinked automatically to /usr/bin, causing idris --install probability.ipkg to fail. This has been fixed by changing it to ~/.cabal/bin/idris --install probability.ipkg.
  • The build status badge in the readme has been fixed.

PR #3 has been opened, which contains all of these changes, which I hope will contribute to the future of this project.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions