Commit Graph

102 Commits

Author SHA1 Message Date
Nicolas Setton
e4c668a9c5 Add support for sandboxing the executables
This relies on an lxc container
2018-07-09 14:35:43 -04:00
Nicolas Setton
adbe60e7ec Replace use of startsWith by indexOf, for compatibility with IE 2018-06-29 15:30:24 -04:00
Nicolas Setton
a5dfe8f511 Fix interruption of long processes. 2018-06-29 13:38:48 -04:00
Nicolas Setton
d14ec2fcb1 Do not count info messages as errors. 2018-06-20 15:17:43 -04:00
Nicolas Setton
ea3a7fc6e7 Add an "universal" spec
Needed to be able to run all combinations of inlined widgets:
with or without SPARK, and with or without main.
2018-06-20 14:28:30 -04:00
Nicolas Setton
dcfa94321c Use -gnata for Ada mains as well. 2018-06-18 15:42:30 -04:00
Nicolas Setton
6378138746 Rename the "Prove" button to "Examine" when in flow mode 2018-06-18 14:27:00 -04:00
Nicolas Setton
e3b31ba99f Add support for making the "info" lines blue
For R525-028
2018-06-18 14:23:18 -04:00
Nicolas Setton
38166ae13a Run SPARK with --level=0 --no-axiom-guard 2018-06-18 14:01:25 -04:00
Nicolas Setton
49fbc93401 Use -gnata when compiling SPARK examples
Requested by Yannick in R525-028.
2018-06-18 13:59:40 -04:00
Nicolas Setton
d134760fed Add Sphinx and Ipython to the requirements
Useful for the development environment.
2018-06-18 11:30:35 -04:00
Nicolas Setton
65b5629234 R525-028 Add features for the SPARK course
Add the ability to pass extra arguments to the prover.
2018-06-05 20:07:47 -04:00
Nicolas Setton
087206674b R525-028 Factor out code
Provision for allowing both "prove" and "run" buttons
on some examples.
2018-06-05 19:35:14 -04:00
Nicolas Setton
cde825d723 Buttons now need to be listed explicitly 2018-06-05 15:31:25 -04:00
Nicolas Setton
e959ffe624 Fix error introduced in refactoring 2018-06-05 15:26:40 -04:00
Nicolas Setton
6f3ba6824c Tentative to stabilize waiting for processes 2018-06-05 15:00:20 -04:00
Nicolas Setton
317c180aee R525-028 Add support for editors with just a 'Run' button
Enable the running backend (in completely unsafe mode for now)
Code cleanup in editors.js.

For inline editors, do not require an AJAX request to get the
example base, assume everything is provided inline.

Add support for providing shadow files: these will not be displayed
in editors but will be transmitted to the backend.
2018-06-05 12:54:01 -04:00
Nicolas Setton
d46e6bd7ae R525-008 Fix regexp for detecting file names 2018-06-02 13:37:36 -04:00
Nicolas Setton
faef8ee40f R525-028 call gnatprove 2018 with --checks-as-errors
Otherwise it reports success even when there are check errors.
2018-06-02 13:28:23 -04:00
Nicolas Setton
41f88d850b Add facility to provide files to a code template
For R525-028.
2018-06-01 21:58:32 -04:00
Nicolas Setton
0905cd2dc7 fixup spark main template 2018-06-01 21:54:23 -04:00
Nicolas Setton
41d10cff79 Add a SPARK Main template 2018-06-01 16:15:24 -04:00
Robert Tice
5c8de067a8 Removing books interface. 2018-04-20 11:01:14 -04:00
Robert Tice
c20c0cc803 updating documentation to include references to new example filling method. 2018-04-20 10:15:47 -04:00
Robert Tice
80c5478fdc Adding script to add examples listed in a conf file. 2018-04-13 10:28:58 -04:00