Open gusthoff opened 6 years ago
As discussed live with Gustavo: This could be a good way to then embed the ouptut of the compiler/run into the resulting PDF version.
Added support for compiler output (for PDF books): #507.
I would like to add to this issue. Currently in the PDF files, you cannot see the commands used to generate the output. Thus, I, as a learner, have no idea what to run in the terminal unless I look somewhere else, such as the online version of the course at hand, to find out.
It would be very nice if all of the terminal output were included, not just the results. E.g.:
$ gprbuild -q -P main.gpr
Build completed successfully.
$ ./learn
Learning Ada from A to Z
Or in the case of SPARK:
$ gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
increment.adb:5:10: info: overflow check proved
increment.ads:4:03: info: data dependencies proved
increment.ads:5:03: info: flow dependencies proved
increment.ads:7:14: info: postcondition proved
increment.ads:7:24: info: overflow check proved
Summary logged in gnatprove/gnatprove.out
Furthermore, all of the examples have example files that can be downloaded. E.g. in the Hello World example in Ada, only the source code of greet.adb is shown. However, the example involves the use of the files main.gpr and main.adc. There is no way to know this just from reading the PDF file. I have made a separate issue about this.
Some source-code examples don't have a "run" button. In those cases, we could still display the output of the compiler and the application statically (i.e., embedded in the HTML page). A "run" button still wouldn't be available in those cases. However, the reader would be able to see the expected output.
One way of implementing this feature could be by (automatically) running the examples on server side and storing the output on a file (on server-side). When the page is accessed on the website, the web-server would merge this output to the remaining HTML code.