WIP Smallstep + Types + STLC + StlcProp

[jutaro]

This pull request is just to make you aware that I try to port the Smallstep chapter. Help welcome and needed.

[clayrat]

Hey, thanks for the help! I'll try to review in the next few days.

[clayrat]

I see you have added the Types chapter, so I changed the name on this PR :)

[jutaro]

Hi Alex,
I will now start to work on the STLC chapter. It would be nice if you find some time to
give feedback and help with my work. I will go to vacations middle of next week.

Here some remarks:

Namespaces:
I see you and Eric did translate modules to namespaces. Actually Idris namespaces seem to me not of
much use: If I understand it right they just make a new name, but you can't say that some namespace
shall not be used or imported. So the compiler always complain and you have to use qualified names,
which is ugly. So I used new names and symbols instead of namespaces, which is ugly as well.

(This caused me problems as well when doing the first chapter exercises, which I couldn't resolve
completely).

Syntax:
I prefered to use operators instead of syntax wherever possible. I used syntax just for Has_type,
(|- a . T), but I can't use it at many positions, because otherwise the compiler complains.
(E.g it reads now: Has_type (Tsucc t) TNat -> |- t . TNat, instead of |- Tsucc t . TNat -> |- t . TNat)

Big versus Small letters:
I tried to use Big Letters for types and constructors but leave everything else as it is. I'm not happy
with the mixture of camelcase and Big and Little letters in use. (E.g. in the Typing chapter:
ttrue is the Term Constructor, which became Ttrue in my translation and T_True is the type assignment constructor.

Implicit aruments:
I'm not shure when to add implicit arguments and when to name them, and things get worse for me for data constructors and type level functions. See for example Multi definition from Smallstep.

Proofs:
I'm currently stuck with the progress proof from types chapter, which is an exercise, so that the difficult part is not visible, if you agree I can send you/show you what I have so far. What I basically don't understand here is to proof, that "x is not a value" so this case is not possible.

Documentation generation:
I managed to install the documentation generation toolchain (Exercise: 5 stars ;)).
I used the most up to date versions of the packages and the following changes become necessary:

In the Makefile PANDOC_FLAGS
--pdf-engine=xelatex instead of --latex-engine=xelatex

As well I would like to add --strip-comments to the PANDOC_FLAGS, because this gives the opportunity to
hide parts with simple HTML comment syntax. (E.g. I skipped the Imp part of Smallstep chapter)

As well I had to take out this two lines from book.tex to make it work:

• \let\RequirePackage\original@RequirePackage
• \let\usepackage\RequirePackage

Can I check the changes in my pull request, or should I do a seperate pull request?

As well sillyfun1_odd from Tactics is not working for minted, and latex can't recover from this. I found some problems with prooftrees in Imp.lidr.

Can I check in the current pdf in my pull request to become already useful for interested learners?

Suggestion:
Link to the pdf/project from the Idris documentation side, as I consider it already the best ressource to learn more about Idris (at least for me it was, and it is difficult to find). Shall I care about this?

Best regards
Jürgen

[yurrriq]

Thanks for this. I’ll try to check it out sometime between tonight and Monday.

[clayrat]

So, just to let you know, I've started reviewing Smallstep at last, got almost halfway through it.

[jutaro]

That fits well, as I start with one more chapter.

[clayrat]

@jutaro I've pushed my WIP post-review fixes for Smallstep directly on this PR, hope you don't mind?

[jutaro]

I scanned your changes, and see that I made some errors with exercises and that the complicated proofs now looks much nicer! I have one problem when compiling, and get the following error, which I don't understand. But I have idris 1.3.0, so maybe I shall upgrade to 1.3.1?

Smallstep.lidr:278:3-65:
|
278 | > step_deterministic ST_PlusConstConst' ST_PlusConstConst' = Refl
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Clauses have differing numbers of arguments

[clayrat]

Oops, pushed an update.

[jutaro]

Now it compiles, you are working on the imperative part. Cool

[clayrat]

Ok I think I'm done with Smallstep, gonna start with Types next.