Marco Vassena
Marco Vassena
I noticed that now the syntax for adding extra arguments is `--latex-args='--synctex=1'`
I can run it, but it doesn't seem to generate the `*synctex.gz` file
The file is written into the output directory (`obj_dir` default `latex.out`). If you need it in the top directory for synching the pdf, pass flag `-O .`.
The fact that PhD students take the course does not make it PhD level. In fact we are allowed to take master level courses for credits as well. But anyway...
I personally do not mind, but there are folks that have never used a proof assistant before and might not get to that level by themselves in in such short...
@AndreasLoow @simonr89 I agree that one should commit to do more than 10 minutes. Splitting a session in, say, two presentations + time for discussion could be reasonable (?) I...