diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py index 675ab9c..3e3396f 100644 --- a/compile_server/app/checker.py +++ b/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) diff --git a/compile_server/app/static/common.css b/compile_server/app/static/common.css index 592f21f..9349465 100644 --- a/compile_server/app/static/common.css +++ b/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; +} diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js index cda006b..d05e05a 100644 --- a/compile_server/app/static/editors.js +++ b/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.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.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 = $('
') - toolbar.appendTo(container) + var row = $('
') + row.appendTo(container) - reset_button = $('