Creating an Idris Track

Exercism Building Exercism
41

The test runner PR passed the workflow.
:slight_smile: I will try to find out if there is a way without skipping --read-only. I guess next step is update the existing exercises to Idris2 and make them confirm to the expectations of the test runner.

1 Like
42

Btw who will review and who have the power to approve and merge the PR to the test runner repo?

43

Erik would be the one generally.

1 Like
44

I am working on migrating the exercises to Idris2 and making them compatible with pack. I am using Tester as testing framework, because it is simple and can be installed with pack. I am keeping an eye on the problem specifications and the Haskell exercises while doing this. If I seem to be doing anything silly, please tell me.

1 Like
45

At a glance, nothing looks silly!

1 Like
46

The documentation is totally out of date though and I plan to completely get rid of everything related to make, because it seems irrelevant when Idris2 specific pack is used. After I have ported the existing 5(?) exercises I will probably look into the of generating tests from the test data in the problem specification. Most likely in Idris.

1 Like
47

The accumulate exercise has been deprecated and there is now the list-ops exercise.

I’m happy to implement

  • all-your-base
  • bob
  • difference-of-squares
  • eliuds-eggs
  • game-of-life
  • pythagorean-triplet
  • scrabble-score
  • reverse-string
2 Likes
48

Sounds great. :slight_smile:

49

I hope to finish the migration of the existing exercises today. They are by no means perfect. Most of all, I am a bit concerned regarding how error messages will turn up to the end user. That relates both to the idris test runner, the test library and how the tests are actually written. It would be great to get feedback on how it actually will look to the end user as soon as possible. :slight_smile:

1 Like
50

There is a few things to clean up: like removing my name from some package files and removing some obsolete files. But then it might be worth considering a merge, especially when we are multiple persons contributing. :slight_smile:

It seems that I cannot say anything more in this thread until someone else does. I have noticed that this PR got automatically closed and that any changes to he branch is not reflected in the PR. This means it would be great if the PR could be opened again for more transparency. @ErikSchierboom or @iHiD.

1 Like
51

It appears that you are not listed as a member of the idris · exercism Team, which is likely why the PR was closed automatically.

1 Like
52

I tried compiling and running leap from your PR with a “first solution attempt”

isLeap year = mod year 4 == 0

and the output was:-

 ... passed
 ... passed
 ... failed
assertEq failed
  left  `True`
  right `False`

 ... passed

passed is in green, failed and a few other words are in red - excellent.

Perhaps the description of the tests (or at least the first failing test) could also be printed:

year divisible by 100, not divisible by 400 in common year

1 Like
53

The CODE RUN block showing what is being tested is also really helpful.

1 Like
54

Thanks @keiraville! That error is not very helpful. I will add a description of the test, as well as improve the error message.

55

@IsaacG is CODE RUN something specific in regards to exercism, or do you mean to just show the assertion that fails?

56

Migrate to idris2 by isberg · Pull Request #134 · exercism/idris · GitHub Recreating because the existing got broken. Still the same branch. @ErikSchierboom

57

I tried rna-transcription with “solution attempt”

toRna = map (\dna => U)

RNA complement of cytosine is guanine
  Test Failed
RNA complement of guanine is cytosine
  Test Failed
RNA complement of thymine is adenine
  Test Failed
RNA complement of adenine is uracil
  Test Passed
RNA complement
  Test Failed

but the process exited with success.

None of this is to suggest the PR shouldn’t be merged. Migration to Idris2 is important progress.

1 Like
58

The PR is now open, there where some config issues, which I hopefully managed to fix, but now the PR needs workflow approval. @iHiD @ErikSchierboom

59

And now a review is needed.

60

@isberg First off: thanks for wanting to revive this track! I’ve always found Idris very interesting (my thesis was on formal verification of software using PVS).

You now have a github invite to join the Idris team, which will give you merge permissions.

@keiraville I’ve also taken the liberty to add you to the Idris team. Let me know if you want that or not.

3 Likes