You've already forked code_examples_server
mirror of
https://github.com/AdaCore/code_examples_server.git
synced 2026-02-12 12:45:18 -08:00
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.
This commit is contained in:
Nicolas Setton
@@ -19,7 +19,7 @@ from compile_server.app.views import CrossDomainResponse
|
||||
gnatprove_found = False
|
||||
gnatemulator_found = False
|
||||
|
||||
ALLOW_RUNNING_PROGRAMS_EVEN_THOUGH_IT_IS_NOT_SECURE = False
|
||||
ALLOW_RUNNING_PROGRAMS_EVEN_THOUGH_IT_IS_NOT_SECURE = True
|
||||
# TODO: right now, executables are run through gnatemulator. We have not
|
||||
# yet done the due diligence to sandbox this, though, so deactivating the
|
||||
# run feature through this boolean.
|
||||
@@ -35,16 +35,6 @@ def check_gnatprove():
|
||||
return gnatprove_found
|
||||
|
||||
|
||||
def check_gnatemulator():
|
||||
"""Check that gnatemulator is found on the PATH"""
|
||||
# Do the check once, for performance
|
||||
global gnatemulator_found
|
||||
if gnatemulator_found:
|
||||
return True
|
||||
gnatemulator_found = distutils.spawn.find_executable("arm-eabi-gnatemu")
|
||||
return gnatemulator_found
|
||||
|
||||
|
||||
@api_view(['POST'])
|
||||
def check_output(request):
|
||||
"""Check the output of a running process."""
|
||||
@@ -153,30 +143,39 @@ def run_program(request):
|
||||
|
||||
# Sanity check for the existence of gnatprove
|
||||
|
||||
if not check_gnatemulator():
|
||||
return CrossDomainResponse({'identifier': '',
|
||||
'message': "gnatemulator not found"})
|
||||
|
||||
received_json = json.loads(request.body)
|
||||
e = get_example(received_json)
|
||||
received_json = json.loads(request.body)
|
||||
|
||||
if not e.main:
|
||||
return CrossDomainResponse(
|
||||
{'identifier': '',
|
||||
'message': "example does not have a main"})
|
||||
|
||||
tempd = prep_example_directory(e, received_json)
|
||||
if not tempd:
|
||||
if not e:
|
||||
return CrossDomainResponse(
|
||||
{'identifier': '', 'message': "example not found"})
|
||||
|
||||
tempd = prep_example_directory(e, received_json)
|
||||
|
||||
# Figure out which is the main
|
||||
if 'main' not in received_json:
|
||||
return CrossDomainResponse(
|
||||
{'identifier': '', 'message': "main not specified"})
|
||||
|
||||
main = received_json['main']
|
||||
|
||||
# In the temporary directory, doctor the project file to know about the
|
||||
# main.
|
||||
|
||||
project_file = os.path.join(tempd, "main.gpr")
|
||||
with codecs.open(project_file, "rb", encoding="utf-8") as f:
|
||||
project_str = f.read()
|
||||
with codecs.open(project_file, "wb", encoding="utf-8") as f:
|
||||
f.write(project_str.replace('@MAIN@', main))
|
||||
|
||||
# Run the command(s) to check the program
|
||||
commands = [
|
||||
["gprbuild", "-q", "-P", "main"],
|
||||
["arm-eabi-gnatemu", "-P", "main", e.main],
|
||||
# TODO: implement a safe execute in a container
|
||||
[os.path.join(tempd, main[:-4])],
|
||||
]
|
||||
|
||||
print commands
|
||||
|
||||
try:
|
||||
p = process_handling.SeparateProcess(commands, tempd)
|
||||
message = "running gnatprove"
|
||||
|
||||
@@ -117,6 +117,7 @@ function query_operation_result(container, example_name, editors, output_area, o
|
||||
|
||||
files = []
|
||||
|
||||
// Grab the contents from actual editors
|
||||
editors.forEach(function (e) {
|
||||
files.push({
|
||||
'basename': e.basename,
|
||||
@@ -124,11 +125,23 @@ function query_operation_result(container, example_name, editors, output_area, o
|
||||
})
|
||||
})
|
||||
|
||||
// Grab the contents from shadow files
|
||||
if (container.shadow_files){
|
||||
container.shadow_files.forEach(function (e){
|
||||
files.push({
|
||||
'basename': e.basename,
|
||||
'contents': e.contents
|
||||
});
|
||||
});
|
||||
}
|
||||
|
||||
data = {
|
||||
"example_name": example_name,
|
||||
"files": files
|
||||
"files": files,
|
||||
"main": container.attr("main")
|
||||
}
|
||||
|
||||
|
||||
// request the examples
|
||||
$.ajax({
|
||||
url: container.example_server + operation_url,
|
||||
@@ -425,144 +438,169 @@ function create_editor(resource, container, content, editors, counter) {
|
||||
|
||||
var unique_id = 0
|
||||
|
||||
function fill_editor_from_contents(container, example_name, example_server,
|
||||
resources, main) {
|
||||
|
||||
is_inline = container.attr("inline")
|
||||
|
||||
// First create the tabs
|
||||
|
||||
if (!is_inline){
|
||||
var ul = $('<ul class="nav nav-tabs" role="tablist">')
|
||||
ul.appendTo(container);
|
||||
|
||||
var counter = 0;
|
||||
|
||||
json.resources.forEach(function (resource) {
|
||||
counter++;
|
||||
var the_id = "tab_" + container.attr("the_id") + "-" + counter
|
||||
|
||||
var li = $('<li role="presentation" class="' +
|
||||
(counter == 1 ? 'active' : '') +
|
||||
'">').appendTo(ul);
|
||||
$('<a href="#' + the_id + '" aria-controls="' +
|
||||
the_id + '" ' +
|
||||
'id="' + the_id + '-tab"' +
|
||||
'role="tab" data-toggle="tab">' +
|
||||
resource.basename + '</a>').appendTo(li)
|
||||
})
|
||||
}
|
||||
|
||||
// Then fill the contents of the tabs
|
||||
|
||||
var content = $('<div class="tab-content">')
|
||||
content.appendTo(container);
|
||||
|
||||
counter = 0;
|
||||
|
||||
var editors = []
|
||||
|
||||
resources.forEach(function (resource) {
|
||||
counter++;
|
||||
editor = create_editor(resource, container, content, editors, counter)
|
||||
// Append the editor to the list of editors
|
||||
editors.push(editor)
|
||||
})
|
||||
|
||||
var row = $('<div class="row output_row">')
|
||||
row.appendTo(container)
|
||||
|
||||
// create the buttons
|
||||
|
||||
var buttons_div = $('<div class="col-md-3">')
|
||||
buttons_div.appendTo(row)
|
||||
|
||||
var output_div = $('<div class="col-md-9">')
|
||||
output_div.appendTo(row)
|
||||
|
||||
var output_area = $('<div class="output_area">')
|
||||
output_area.appendTo(output_div)
|
||||
|
||||
if (container.attr("prove_button") || container.attr("run_button")){
|
||||
var reset_button = $('<button type="button" class="btn btn-secondary">').text("Reset").appendTo(buttons_div)
|
||||
reset_button.editors = editors;
|
||||
reset_button.on('click', function (x) {
|
||||
output_area.empty();
|
||||
output_area.error_count = 0;
|
||||
|
||||
reset_button.editors.forEach(function (x) {
|
||||
x.setValue(x.initial_contents);
|
||||
x.gotoLine(1);
|
||||
})
|
||||
})
|
||||
}
|
||||
|
||||
if (container.attr("prove_button")){
|
||||
var check_button = $('<button type="button" class="btn btn-primary">').text("Prove").appendTo(buttons_div)
|
||||
check_button.editors = editors;
|
||||
check_button.on('click', function (x) {
|
||||
output_area.empty();
|
||||
output_area.error_count = 0;
|
||||
|
||||
var div = $('<div class="output_info">');
|
||||
div.text("Proving...");
|
||||
div.appendTo(output_area);
|
||||
query_operation_result(container, example_name, check_button.editors, output_area, "/check_program/");
|
||||
})
|
||||
}
|
||||
|
||||
if (container.attr("run_button")){
|
||||
var run_button = $('<button type="button" class="btn btn-primary">').text("Run").appendTo(buttons_div);
|
||||
run_button.editors = editors;
|
||||
run_button.on('click', function (x) {
|
||||
output_area.empty();
|
||||
output_area.error_count = 0;
|
||||
|
||||
var div = $('<div class="output_info">');
|
||||
div.text("Running...");
|
||||
div.appendTo(output_area);
|
||||
query_operation_result(container, example_name, run_button.editors, output_area, "/run_program/");
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
function fill_editor(container, example_name, example_server) {
|
||||
unique_id++;
|
||||
container.attr("the_id", unique_id);
|
||||
container.example_server = example_server;
|
||||
|
||||
is_inline = container.attr("inline");
|
||||
|
||||
// request the examples
|
||||
$.ajax({
|
||||
url: container.example_server + "/example/" + example_name,
|
||||
data: {},
|
||||
type: "GET",
|
||||
// dataType : "json",
|
||||
contentType: 'text/plain',
|
||||
crossDomain: true,
|
||||
// headers: { "Origin": "http://www.adacore.com" }
|
||||
if (is_inline){
|
||||
// In inline mode, just assume all the sources are here, do not
|
||||
// request them in AJAX
|
||||
|
||||
})
|
||||
.done(function (json) {
|
||||
// On success, create editors for each of the resources
|
||||
// List the "file" divs, add these as resources
|
||||
var resources = []
|
||||
$(container).children(".file").each(function () {
|
||||
// Create a fake resource for each 'file' div
|
||||
a = Object();
|
||||
a.basename = $(this).attr("basename");
|
||||
a.contents = $(this).text();
|
||||
$(this).text('');
|
||||
resources.push(a);
|
||||
})
|
||||
|
||||
$(container).children(".file").each(function () {
|
||||
// Create a fake resource for each 'file' div
|
||||
a = Object();
|
||||
a.basename = $(this).attr("basename");
|
||||
a.contents = $(this).text();
|
||||
$(this).text('');
|
||||
json.resources.push(a);
|
||||
})
|
||||
// List the contents of the ".shadow_file" divs
|
||||
container.shadow_files = []
|
||||
$(container).children(".shadow_file").each(function () {
|
||||
// Create a fake resource for each 'file' div
|
||||
a = Object();
|
||||
a.basename = $(this).attr("basename");
|
||||
a.contents = $(this).text();
|
||||
$(this).text('');
|
||||
container.shadow_files.push(a);
|
||||
})
|
||||
|
||||
// First create the tabs
|
||||
is_inline = container.attr("inline")
|
||||
fill_editor_from_contents(container, example_name, example_server,
|
||||
resources, container.attr("main"));
|
||||
} else {
|
||||
|
||||
if (!is_inline){
|
||||
var ul = $('<ul class="nav nav-tabs" role="tablist">')
|
||||
ul.appendTo(container);
|
||||
// request the examples
|
||||
$.ajax({
|
||||
url: container.example_server + "/example/" + example_name,
|
||||
data: {},
|
||||
type: "GET",
|
||||
// dataType : "json",
|
||||
contentType: 'text/plain',
|
||||
crossDomain: true,
|
||||
// headers: { "Origin": "http://www.adacore.com" }
|
||||
|
||||
var counter = 0;
|
||||
})
|
||||
.done(function (json) {
|
||||
// On success, create editors for each of the resources
|
||||
|
||||
json.resources.forEach(function (resource) {
|
||||
counter++;
|
||||
var the_id = "tab_" + container.attr("the_id") + "-" + counter
|
||||
fill_editor_from_contents(container, example_name, example_server,
|
||||
json.resources, json.main);
|
||||
|
||||
var li = $('<li role="presentation" class="' +
|
||||
(counter == 1 ? 'active' : '') +
|
||||
'">').appendTo(ul);
|
||||
$('<a href="#' + the_id + '" aria-controls="' +
|
||||
the_id + '" ' +
|
||||
'id="' + the_id + '-tab"' +
|
||||
'role="tab" data-toggle="tab">' +
|
||||
resource.basename + '</a>').appendTo(li)
|
||||
})
|
||||
}
|
||||
|
||||
// Then fill the contents of the tabs
|
||||
|
||||
var content = $('<div class="tab-content">')
|
||||
content.appendTo(container);
|
||||
|
||||
counter = 0;
|
||||
|
||||
var editors = []
|
||||
|
||||
json.resources.forEach(function (resource) {
|
||||
counter++;
|
||||
editor = create_editor(resource, container, content, editors, counter)
|
||||
// Append the editor to the list of editors
|
||||
editors.push(editor)
|
||||
})
|
||||
|
||||
var row = $('<div class="row output_row">')
|
||||
row.appendTo(container)
|
||||
|
||||
// create the buttons
|
||||
|
||||
var buttons_div = $('<div class="col-md-3">')
|
||||
buttons_div.appendTo(row)
|
||||
|
||||
var reset_button = $('<button type="button" class="btn btn-secondary">').text("Reset").appendTo(buttons_div)
|
||||
reset_button.editors = editors
|
||||
|
||||
var check_button = $('<button type="button" class="btn btn-primary">').text("Prove").appendTo(buttons_div)
|
||||
check_button.editors = editors
|
||||
// Create the output area
|
||||
|
||||
if (json.main) {
|
||||
run_button = $('<button type="button" class="btn btn-primary">').text("Run").appendTo(buttons_div)
|
||||
run_button.editors = editors
|
||||
}
|
||||
|
||||
var output_div = $('<div class="col-md-9">')
|
||||
output_div.appendTo(row)
|
||||
|
||||
var output_area = $('<div class="output_area">')
|
||||
output_area.appendTo(output_div)
|
||||
|
||||
// Connect the buttons
|
||||
reset_button.on('click', function (x) {
|
||||
output_area.empty()
|
||||
output_area.error_count = 0
|
||||
|
||||
reset_button.editors.forEach(function (x) {
|
||||
x.setValue(x.initial_contents)
|
||||
x.gotoLine(1)
|
||||
})
|
||||
})
|
||||
|
||||
check_button.on('click', function (x) {
|
||||
output_area.empty()
|
||||
output_area.error_count = 0
|
||||
|
||||
var div = $('<div class="output_info">')
|
||||
div.text("Proving...")
|
||||
div.appendTo(output_area)
|
||||
query_operation_result(container, example_name, check_button.editors, output_area, "/check_program/")
|
||||
})
|
||||
|
||||
if (json.main) {
|
||||
run_button.on('click', function (x) {
|
||||
output_area.empty()
|
||||
output_area.error_count = 0
|
||||
|
||||
var div = $('<div class="output_info">')
|
||||
div.text("Running...")
|
||||
div.appendTo(output_area)
|
||||
query_operation_result(container, example_name, check_button.editors, output_area, "/run_program/")
|
||||
})
|
||||
}
|
||||
})
|
||||
.fail(function (xhr, status, errorThrown) {
|
||||
//
|
||||
alert("could not download the example");
|
||||
console.log("Error: " + errorThrown);
|
||||
console.log("Status: " + status);
|
||||
console.dir(xhr);
|
||||
});
|
||||
// Code to run regardless of success or failure;
|
||||
// commented for now - just so I remember how it's done
|
||||
// .always(function( xhr, status ) {});
|
||||
.fail(function (xhr, status, errorThrown) {
|
||||
alert("could not download the example");
|
||||
console.log("Error: " + errorThrown);
|
||||
console.log("Status: " + status);
|
||||
console.dir(xhr);
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
2
resources/templates/ada_main/example.yaml
Normal file
2
resources/templates/ada_main/example.yaml
Normal file
@@ -0,0 +1,2 @@
|
||||
name: Ada Main
|
||||
description: Simple overrideable runnable main
|
||||
13
resources/templates/ada_main/main.gpr
Normal file
13
resources/templates/ada_main/main.gpr
Normal file
@@ -0,0 +1,13 @@
|
||||
project Main is
|
||||
|
||||
for Main use ("@MAIN@");
|
||||
|
||||
package Compiler is
|
||||
for Switches ("ada") use ("-g");
|
||||
end Compiler;
|
||||
|
||||
package Builder is
|
||||
for Switches ("ada") use ("-g", "-O0");
|
||||
end Builder;
|
||||
|
||||
end Main;
|
||||
@@ -1 +0,0 @@
|
||||
abdasd.adb:1:01: compilation unit expected
|
||||
@@ -1 +0,0 @@
|
||||
|
||||
@@ -1,71 +0,0 @@
|
||||
[main]
|
||||
magic = 14
|
||||
memlimit = 0
|
||||
[editor coqide]
|
||||
name = "CoqIDE"
|
||||
command = "coqide -I %l/coq-tactic -R %o/why3_libs/coq Why3 %f"
|
||||
[prover]
|
||||
command = "alt-ergo -max-split 5 %f"
|
||||
command_steps = "alt-ergo -steps-bound %S -max-split 5 %f"
|
||||
driver = "alt-ergo_gnatprove.drv"
|
||||
name = "altergo"
|
||||
shortcut = "altergo"
|
||||
version = "1.30-gnatprove"
|
||||
[prover]
|
||||
command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
driver = "cvc4_gnatprove.drv"
|
||||
name = "CVC4"
|
||||
shortcut = "cvc4"
|
||||
version = "1.6-gnatprove"
|
||||
[prover]
|
||||
command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
driver = "cvc4_gnatprove_extra_axioms.drv"
|
||||
name = "CVC4_More_Axioms"
|
||||
shortcut = "cvc4_axioms"
|
||||
version = "1.6-gnatprove"
|
||||
[prover]
|
||||
command = "cvc4 --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
|
||||
driver = "cvc4_gnatprove_qf.drv"
|
||||
name = "CVC4_QF"
|
||||
shortcut = "cvc4_qf"
|
||||
version = "1.6-gnatprove"
|
||||
[prover]
|
||||
command = "cvc4 --tlimit-per=%t000 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
|
||||
command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
|
||||
driver = "cvc4_gnatprove_ce.drv"
|
||||
name = "CVC4_CE"
|
||||
shortcut = "cvc4_ce"
|
||||
version = "1.6-gnatprove"
|
||||
[prover]
|
||||
command = "z3 -smt2 -st %f"
|
||||
command_steps = "z3 rlimit=%S -smt2 -st %f"
|
||||
driver = "z3_gnatprove.drv"
|
||||
name = "Z3"
|
||||
shortcut = "z3"
|
||||
version = "4.5.1-gnatprove"
|
||||
[prover]
|
||||
command = "z3 -smt2 -st %f"
|
||||
command_steps = "z3 rlimit=%S -smt2 -st %f"
|
||||
driver = "z3_no_quant.drv"
|
||||
name = "Z3_noquant"
|
||||
shortcut = "z3_noquant"
|
||||
version = "4.5.1-gnatprove"
|
||||
[prover]
|
||||
command = "z3 -t:%t -smt2 -st %f"
|
||||
command_steps = "z3 rlimit=%S -smt2 -st %f"
|
||||
driver = "z3_gnatprove_ce.drv"
|
||||
name = "z3_ce"
|
||||
shortcut = "z3_ce"
|
||||
version = "4.5.1-gnatprove"
|
||||
[prover]
|
||||
command = "coqtop -batch -I %l/coq-tactic -R %o/why3_libs/coq Why3 -l %f"
|
||||
driver = "coq_gnatprove.drv"
|
||||
name = "Coq"
|
||||
shortcut = "coq"
|
||||
version = "8.5pl2"
|
||||
interactive = true
|
||||
editor = "coqide"
|
||||
in_place = false
|
||||
Reference in New Issue
Block a user