search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.37k stars 315 forks source link

Holey version of PLFA? #1026

Closed JacquesCarette closed 2 months ago

JacquesCarette commented 2 months ago

Context: as with others, I teach using PLFA via live coding. So I need a 'holey' version that has most of the text stripped out, and holes judiciously inserted. It is also convenient to have some of the 'clever' spacing removed because screen real estate is much more dear in such a setting.

Problem: This is a tedious by-hand process that has to be redone when PLFA evolves.

Questions:

  1. Should version-stamped copies of holey-PLFA be saved in the PLFA repo, to help like-minded instructors?
  2. Should there be some kind of less tedious process to produce such a version be created?
wadler commented 2 months ago

I also use live coding, but never found any of these to be a problem. Could you say more about what kind of 'holey-PLFA' you'd like available in the repo, and what kind of process you think might be used?

wenkokke commented 2 months ago

Context: as with others, I teach using PLFA via live coding. So I need a 'holey' version that has most of the text stripped out, and holes judiciously inserted. It is also convenient to have some of the 'clever' spacing removed because screen real estate is much more dear in such a setting.

Problem: This is a tedious by-hand process that has to be redone when PLFA evolves.

Questions:

  1. Should version-stamped copies of holey-PLFA be saved in the PLFA repo, to help like-minded instructors?

  2. Should there be some kind of less tedious process to produce such a version be created?

My guess is that it's going to be hard to develop a "holey" version that satisfies everyone's teaching styles.

wenkokke commented 2 months ago

I'd veto committing a separate "holey" version to the repository, since keeping it in sync would effectively double the maintenance burden.

I'm uncertain about committing a set of scripts to generate such a thing. Scripts tend to be added to PLFA and then die due to increasing complexity and lack of external maintenance. (See, e.g. what happened to PDF generation.)

wenkokke commented 2 months ago

That said, Phil commits his course files to the repository.

I'd be happy for you to add the "holey" version that you use for live coding, under the understanding that it's associated with one particular course, and not maintained.

wadler commented 2 months ago

Just to clarify, the course files Wen refers to are in courses/TSPL/<year>. If Jacques wants to store holey files, or anything else, in courses/<name-of-Jacques-course>/<year> he would be most welcome to do so, and that would make any resources there available to other PLFA users.

JacquesCarette commented 2 months ago

Right, associating it with a particular course as opposed to something that needs maintained seems like a good compromise between all the factors at at play. I'll proceed to do that once I have my files ready.