3 ms·

Mostly Automated Proof Repair for Verified Libraries [pdf]

33 points by ghuntley 3y ago

staunton 3y ago
Sounds like a pretty nice achievement. On another note, I'm increasingly amazed how researchers seem to persist in using ugly PDFs to publish their work. I cam understand e.g. biologists doing it, but when CS folks who should know alternatives do it, I'm evermore baffled, especially given the awkwardness of using e.g. LaTeX.
- deleted 3y ago
  [deleted]
- funcDropShadow 3y ago
  What would be an alternative? A web page? LaTeX has a steep learning curve, but it is very well understood, it doesn't churn needlessly. That is extremely valuable if you don't want to spend your time learning again and again how to do the same thing this week. PDF with all its problems are also well understood, they can be archived. Some nation states require certain documents to be archived in PDF. I.e. you can be relatively sure that there will be PDF readers in 50 or 100 years that can display and print our PDFs. I have my doubts whether it will be possible to display a modern web page of today in a browser in 100 years without constantly maintaining the web page. > I cam understand e.g. biologists doing it, but when CS folks who should know alternatives do it, I'm evermore baffled, especially given the awkwardness of using e.g. LaTeX. In my experience it is the other way around: mathematicians, computer scientists and physicists are those using LaTeX the most. Probably, because they are already familiar with programming languages. Hence a markup language is less of a hurdle for them. But have you tried setting math in something else than LaTeX? LaTeX is still the gold standard for math formulas. Or consider lecture slides. Professors often want to develop their slides over one or two decades. Just imagine using PowerPoint to manage a few thousand slides (one course over a semester). And imagine keeping that file in a workable state over a decade in PowerPoint. Good luck. Whereas it is no problem to do that with LaTeX and git.
  - staunton 3y ago
    I fully agree that churning out some LaTeX PDFs isn't that cumbersome compared to doing a website, for example. When you already have a workflow for PDFs, which you can pass down generations of students, doing more is work. However, I'm surprised readers don't strongly favor other formats. Doing a more modern website enables a lot of things that PDFs cannot do. Animations, interactivity, better automatic parsing, metadata generation, tracking of changes and versions, easier embedding elsewhere, better referencing and citing (hyperlinks), even automatically verifiable, etc. In a PDF, even marking and copying text often doesn't work properly. Maybe people who write papers mostly don't (have to) care about presentation of the content? Then again, "quality of figures identifies 90% of any paper's merit" because people don't read the text. This is what confuses me. Why don't readers strongly prefer non-PDF publications, of if they do, why don't they get what they want? Mind you, I strongly expect PDFs to become old-fashioned and eventually obsolete for publishing research anyway.
    - SiempreViernes 3y ago
      Because most contents you find on the web is of even worse quality than what you find in pdf's (provided you read on a big screen).
    - auggierose 3y ago
      I agree that the potential of a modern website is bigger than that of a PDF. The problem is that the effort to get there is much much MUCH bigger than with a PDF. A PDF has the advantage that it gives the reader a high quality product, consistently. I love reading PDFs on a large iPad. As a reader, these are my highest priorities: * high quality (proper layout & design, high resolution of graphics and text) * easy to store in my library, so I can read it again whenever I want to PDF does that. A modern website acceptable to me needs to do that at least as well as PDF does. And they usually don't. For example, how would I store that website easily in my library, being sure that it doesn't depend on some weird JS library downloaded from an obsolete Cloudflare link? The ePub standard is supposed to deliver that, but it falls short in practice. Whenever there is both an ePub version of something, and a PDF version, I choose the PDF version, because it is just easier and more pleasant to read. An exception are books consisting of purely text like novels, which is where I prefer ePubs.

33 points by ghuntley 3y ago

Sounds like a pretty nice achievement. On another note, I'm increasingly amazed how researchers seem to persist in using ugly PDFs to publish their work. I cam understand e.g. biologists doing it, but when CS folks who should know alternatives do it, I'm evermore baffled, especially given the awkwardness of using e.g. LaTeX.

deleted 3y ago
[deleted]
funcDropShadow 3y ago
What would be an alternative? A web page? LaTeX has a steep learning curve, but it is very well understood, it doesn't churn needlessly. That is extremely valuable if you don't want to spend your time learning again and again how to do the same thing this week. PDF with all its problems are also well understood, they can be archived. Some nation states require certain documents to be archived in PDF. I.e. you can be relatively sure that there will be PDF readers in 50 or 100 years that can display and print our PDFs. I have my doubts whether it will be possible to display a modern web page of today in a browser in 100 years without constantly maintaining the web page. > I cam understand e.g. biologists doing it, but when CS folks who should know alternatives do it, I'm evermore baffled, especially given the awkwardness of using e.g. LaTeX. In my experience it is the other way around: mathematicians, computer scientists and physicists are those using LaTeX the most. Probably, because they are already familiar with programming languages. Hence a markup language is less of a hurdle for them. But have you tried setting math in something else than LaTeX? LaTeX is still the gold standard for math formulas. Or consider lecture slides. Professors often want to develop their slides over one or two decades. Just imagine using PowerPoint to manage a few thousand slides (one course over a semester). And imagine keeping that file in a workable state over a decade in PowerPoint. Good luck. Whereas it is no problem to do that with LaTeX and git.
- staunton 3y ago
  I fully agree that churning out some LaTeX PDFs isn't that cumbersome compared to doing a website, for example. When you already have a workflow for PDFs, which you can pass down generations of students, doing more is work. However, I'm surprised readers don't strongly favor other formats. Doing a more modern website enables a lot of things that PDFs cannot do. Animations, interactivity, better automatic parsing, metadata generation, tracking of changes and versions, easier embedding elsewhere, better referencing and citing (hyperlinks), even automatically verifiable, etc. In a PDF, even marking and copying text often doesn't work properly. Maybe people who write papers mostly don't (have to) care about presentation of the content? Then again, "quality of figures identifies 90% of any paper's merit" because people don't read the text. This is what confuses me. Why don't readers strongly prefer non-PDF publications, of if they do, why don't they get what they want? Mind you, I strongly expect PDFs to become old-fashioned and eventually obsolete for publishing research anyway.
  - SiempreViernes 3y ago
    Because most contents you find on the web is of even worse quality than what you find in pdf's (provided you read on a big screen).
  - auggierose 3y ago
    I agree that the potential of a modern website is bigger than that of a PDF. The problem is that the effort to get there is much much MUCH bigger than with a PDF. A PDF has the advantage that it gives the reader a high quality product, consistently. I love reading PDFs on a large iPad. As a reader, these are my highest priorities: * high quality (proper layout & design, high resolution of graphics and text) * easy to store in my library, so I can read it again whenever I want to PDF does that. A modern website acceptable to me needs to do that at least as well as PDF does. And they usually don't. For example, how would I store that website easily in my library, being sure that it doesn't depend on some weird JS library downloaded from an obsolete Cloudflare link? The ePub standard is supposed to deliver that, but it falls short in practice. Whenever there is both an ePub version of something, and a PDF version, I choose the PDF version, because it is just easier and more pleasant to read. An exception are books consisting of purely text like novels, which is where I prefer ePubs.