diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py
index 2d6d2db..ff57ac4 100644
--- a/compile_server/app/checker.py
+++ b/compile_server/app/checker.py
@@ -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"
diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index 72539a0..eb6258f 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -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);
+           });
+        }
 }
 
 
diff --git a/resources/templates/ada_main/example.yaml b/resources/templates/ada_main/example.yaml
new file mode 100644
index 0000000..772e99a
--- /dev/null
+++ b/resources/templates/ada_main/example.yaml
@@ -0,0 +1,2 @@
+name: Ada Main
+description: Simple overrideable runnable main
diff --git a/resources/templates/ada_main/main.gpr b/resources/templates/ada_main/main.gpr
new file mode 100644
index 0000000..6537074
--- /dev/null
+++ b/resources/templates/ada_main/main.gpr
@@ -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;
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stderr b/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
deleted file mode 100644
index 09b0a52..0000000
--- a/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
+++ /dev/null
@@ -1 +0,0 @@
-abdasd.adb:1:01: compilation unit expected
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stdout b/resources/templates/spark_main/gnatprove/abdasd.adb.stdout
deleted file mode 100644
index e69de29..0000000
diff --git a/resources/templates/spark_main/gnatprove/gnatprove.out b/resources/templates/spark_main/gnatprove/gnatprove.out
deleted file mode 100644
index 8b13789..0000000
--- a/resources/templates/spark_main/gnatprove/gnatprove.out
+++ /dev/null
@@ -1 +0,0 @@
-
diff --git a/resources/templates/spark_main/gnatprove/why3.conf b/resources/templates/spark_main/gnatprove/why3.conf
deleted file mode 100644
index b3c4b2b..0000000
--- a/resources/templates/spark_main/gnatprove/why3.conf
+++ /dev/null
@@ -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