Implement the code checker

The 'Check' button now launches GNATprove

compile_server/app/checker.py

@@ -1,15 +1,43 @@
 # -*- coding: utf-8 -*-
 
+import os
+import codecs
+import distutils.spawn
 import json
+import shutil
+import subprocess
+import tempfile
 
 from rest_framework.response import Response
 from rest_framework.decorators import api_view
 
 from compile_server.app.models import Resource, Example
 
+gnatprove_found = False
+
+
+def check_gnatprove():
+    """Check that gnatprove is found on the PATH"""
+    # Do the check once, for performance
+    global gnatprove_found
+    if gnatprove_found:
+        return True
+    gnatprove_found = distutils.spawn.find_executable("gnatprove")
+    return gnatprove_found
+
 
 @api_view(['POST'])
 def check_program(request):
+
+    # Sanity check for the existence of gnatprove
+
+    if not check_gnatprove():
+        result = {'output': "gnatprove not found",
+                  'status': 0,
+                  'message': "error"}
+
+        return Response(result)
+
     received_json = json.loads(request.body)
 
     matches = Example.objects.filter(name=received_json['example_name'])
@@ -18,7 +46,58 @@ def check_program(request):
         return Response()
 
     e = matches[0]
-    print received_json
-    print e
-    result = {'output': "bla\nbla\nbla"}
+
+    output = ""
+    status = 0
+    message = "an error occurred while checking the program"
+
+    try:
+        # Create a temporary directory
+        tempd = tempfile.mkdtemp()
+
+        # Copy the original resources in a sandbox directory
+        target = os.path.join(tempd, os.path.basename(e.original_dir))
+        shutil.copytree(e.original_dir, target)
+
+        # Overwrite with the user-contributed files
+        for file in received_json['files']:
+            with codecs.open(os.path.join(target, file['basename']),
+                             'w', 'utf-8') as f:
+                f.write(file['contents'])
+
+        # TODO: find a command to just check rather than build
+        command = ["gnatprove", "-P", "main"]
+
+        # Run the command(s) to check the program
+        try:
+            output = subprocess.check_output(
+                command,
+                stderr=subprocess.STDOUT,
+                cwd=target)
+            message = "success"
+
+        except subprocess.CalledProcessError, exception:
+            output = exception.output
+            message = "error"
+            status = exception.returncode
+
+    finally:
+
+        # Cleanup
+        shutil.rmtree(tempd)
+
+    output_lines = []
+    for l in output.splitlines():
+        # Suppress some gnatprove output that's noise for this application
+        if not l.startswith("Summary logged"):
+            output_lines.append(l)
+
+    # Send the result back
+
+    result = {'output_lines': output_lines,
+              'status': status,
+              'message': message}
+
+    print result
+
     return Response(result)

compile_server/app/static/common.css

@@ -3,3 +3,25 @@ div.editor_container{
    border: 1px solid #ddd;
    border-top: 0px;
 }
+
+div.output_line{
+   color: #666;
+   padding-left:3px;
+   padding-right:3px;
+}
+
+div.output_msg{
+   color: #944;
+   padding-left:3px;
+   padding-right:3px;
+}
+
+div.output_msg:hover{
+   background-color:#fdd;
+}
+
+div.output_success{
+   color: #494;
+   padding-left:3px;
+   padding-right:3px;
+}

compile_server/app/static/editors.js

@@ -1,5 +1,54 @@
+// Process the result of a check
+//  editors: the editors to decorate
+//  output_area: the div where the messages should go
+//  status: the exit status
+//  message: any message coming back from the application
+//   TODO: make use of message
+function process_check_output(editors, output_area, output, status, message){
+
+   // Clear the output area
+   output_area.empty()
+
+   // Process the lines
+   output.forEach(function (l){
+      // Look for lines that contain an error message
+      var match_found = l.match(/^([a-zA-Z._-]+):(\d+):(\d+):(.+)$/)
+      var klass = match_found?"output_msg":"output_line"
+
+      // Print the line in the output area
+      var div = $('<div class="' + klass + '">')
+      div.text(l)
+      div.appendTo(output_area)
+
+      if (match_found != null){
+         // Lines that contain a sloc are clickable:
+         div.on('click', function(x){
+            // find the corresponding editor
+            var basename = match_found[1]
+            editors.forEach(function (e){
+               if (e.basename == basename){
+                  // Switch to the tab that contains the editor
+                  $("#" + e.unique_id + "-tab").tab('show')
+
+                  // Jump to the corresponding line
+                  e.gotoLine(parseInt(match_found[2]),
+                             parseInt(match_found[3]), true)
+               }
+            })
+         })
+       }
+    })
+
+    // Congratulations!
+    if (status == 0){
+      var div = $('<div class="output_success">')
+      div.text("Success!")
+      div.appendTo(output_area)
+    }
+}
+
 // Launch a check on the given example editor
-function query_check_result(example_name, editors, container) {
+function query_check_result(example_name, editors, output_area) {
 
    files = []
 
@@ -20,7 +69,8 @@ function query_check_result(example_name, editors, container) {
       contentType: 'application/json; charset=UTF-8',
    })
    .done(function( json ) {
-      alert(json)
+      process_check_output(editors, output_area,
+         json.output_lines, json.status, json.message)
    })
    .fail(function( xhr, status, errorThrown ) {
      //
@@ -94,7 +144,6 @@ function fill_editor(container, example_name) {
           editordiv.appendTo(div)
           div.appendTo(content);
 
-
           // ACE editors...
           var editor = ace.edit(resource.basename + the_id + '_editor')
           editor.session.setMode("ace/mode/ada");
@@ -104,6 +153,7 @@ function fill_editor(container, example_name) {
           editor.gotoLine(1)
           editor.initial_contents = resource.contents
           editor.basename = resource.basename
+          editor.unique_id = the_id
 
           // TODO: place the cursor at 1,1
 
@@ -111,23 +161,48 @@ function fill_editor(container, example_name) {
           editors.push(editor)
       })
 
-      var toolbar = $('<div class="btn-toolbar">')
-      toolbar.appendTo(container)
+      var row = $('<div class="row">')
+      row.appendTo(container)
 
-      reset_button = $('<button type="button" class="btn btn-secondary">').text("Reset").appendTo(toolbar)
+      // create the buttons
+
+      var buttons_div = $('<div class="col-md-2">')
+      buttons_div.appendTo(row)
+
+      reset_button = $('<button type="button" class="btn btn-secondary">'
+         ).text("Reset").appendTo(buttons_div)
       reset_button.editors = editors
+
+      check_button = $('<button type="button" class="btn btn-primary">'
+         ).text("Check").appendTo(buttons_div)
+      check_button.editors = editors
+      // Create the output area
+
+      var output_div = $('<div class="col-md-8">')
+      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()
+
           reset_button.editors.forEach(function (x){
              x.setValue(x.initial_contents)
              x.gotoLine(1)
           })
       })
 
-      check_button = $('<button type="button" class="btn btn-primary">').text("Check").appendTo(toolbar)
-      check_button.editors = editors
       check_button.on('click', function (x){
-         query_check_result(example_name, check_button.editors, container)
+         output_area.empty()
+
+         // TODO: animate this
+         $('<span>').text("Checking...").appendTo(output_area)
+         query_check_result(example_name, check_button.editors, output_area)
       })
+
+
    })
    .fail(function( xhr, status, errorThrown ) {
      //