Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

agda2vec introduces extra empty lines #653

Open
carlostome opened this issue Jan 28, 2025 · 1 comment · May be fixed by #666
Open

agda2vec introduces extra empty lines #653

carlostome opened this issue Jan 28, 2025 · 1 comment · May be fixed by #666
Assignees
@williamdemeo
Labels
bug Something isn't working

Comments

@carlostome
Copy link
Contributor

Running

agda --latex Ex.lagda
python agda2vec.py latex/Ex.tex latex/Bad.tex
latexmk -cd -pdfxe latex/Bad.tex

on a file Ex.lagda that contains

\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}[hide]
module Ex where
\end{code}[hide]

\begin{code}
data T : Set where
  t : T
\end{code}

\end{document}

produces an error

! LaTeX Error: There's no line here to end.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...

l.47 \end{code}

However, running latexmk -cd -pdfxe latex/Ex.tex does not.
I think the culprit is that agda2vec.py introduces many empty lines (compare latex/Ex.tex to latex/Bad.tex).
@WhatisRT WhatisRT added the bug Something isn't working label Jan 28, 2025
@carlostome carlostome mentioned this issue Jan 29, 2025
Open
4 tasks
@williamdemeo
Copy link
Collaborator

williamdemeo commented Jan 31, 2025 •
edited
Loading

It seems removing + \n from the file.write line in the write_file function may fix this... but there must be some reason I added that initially. I'm running the script on the whole formal spec pdf (without the + \n) to see if it works okay. If it does I'll make a PR with that change asap.

williamdemeo added a commit that referenced this issue Jan 31, 2025
@williamdemeo
agda2vec introduces extra empty lines #653
2a69366 
This closes issue #653.

(It may be as simple as removing the extra new line character `+ \n` from the `file.write` line in the `write_file` function.)
@williamdemeo williamdemeo linked a pull request Jan 31, 2025 that will close this issue
agda2vec introduces extra empty lines #666
Draft
4 tasks
@williamdemeo williamdemeo linked a pull request Jan 31, 2025 that will close this issue
Draft
4 tasks
@williamdemeo williamdemeo self-assigned this Jan 31, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@williamdemeo williamdemeo

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

agda2vec introduces extra empty lines IntersectMBO/formal-ledger-specifications
3 participants
@WhatisRT @carlostome @williamdemeo