Initial revision of checker, work in progress

compile_server/app/checker.py

@@ -0,0 +1,24 @@
+# -*- coding: utf-8 -*-
+
+import json
+
+from rest_framework.response import Response
+from rest_framework.decorators import api_view
+
+from compile_server.app.models import Resource, Example
+
+
+@api_view(['POST'])
+def check_program(request):
+    received_json = json.loads(request.body)
+
+    matches = Example.objects.filter(name=received_json['example_name'])
+
+    if not matches:
+        return Response()
+
+    e = matches[0]
+    print received_json
+    print e
+    result = {'output': "bla\nbla\nbla"}
+    return Response(result)

compile_server/app/management/commands/fill_examples.py

@@ -67,6 +67,7 @@ class Command(BaseCommand):
                         resources.append(r)
 
             e = Example(description=metadata['description'],
+                        original_dir=d,
                         name=metadata['name'])
             e.save()
             e.resources.add(*resources)

compile_server/app/models.py

@@ -40,5 +40,8 @@ class Example(models.Model):
     # A description
     description = models.TextField()
 
+    # The directory which contains the original contents
+    original_dir = models.TextField()
+
     # An example is a contains a set of resources
     resources = models.ManyToManyField(Resource)

compile_server/app/serializers.py

@@ -1,6 +1,6 @@
 from django.contrib.auth.models import User, Group
 from rest_framework import serializers
-from compile_server.app.models import Resource
+from compile_server.app.models import Resource, Example
 
 
 class UserSerializer(serializers.HyperlinkedModelSerializer):
@@ -31,3 +31,9 @@ class ResourceSerializer(serializers.Serializer):
         instance.basename = validated_data.get('basename', instance.basename)
         instance.save()
         return instance
+
+
+class ExampleSerializer(serializers.ModelSerializer):
+    class Meta:
+        model = Example
+        fields = ('name', 'description')

compile_server/app/static/editors.js

@@ -1,4 +1,5 @@
-function query_check_result(editors, container) {
+// Launch a check on the given example editor
+function query_check_result(example_name, editors, container) {
 
    files = []
 
@@ -7,7 +8,8 @@ function query_check_result(editors, container) {
                    'contents': e.getValue()})
    })
 
-   data = {"files": files}
+   data = {"example_name": example_name,
+           "files": files}
 
    // request the examples
    $.ajax({
@@ -124,7 +126,7 @@ function fill_editor(container, example_name) {
       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(check_button.editors, container)
+         query_check_result(example_name, check_button.editors, container)
       })
    })
    .fail(function( xhr, status, errorThrown ) {

compile_server/app/templates/code_page.html

@@ -1,7 +1,9 @@
 {% extends 'base.html' %}
 {% block content %}
 
- <h3>{{ example_name }}</h3>
- <div example_editor="{{ example_name }}"></div>
+ <h3>{{ example.name }}</h3>
+ {{ example.description }}
+ <p></p>
+ <div example_editor="{{ example.name }}"></div>
 
 {% endblock%}

compile_server/app/views.py

@@ -13,7 +13,8 @@ from rest_framework.decorators import api_view
 from rest_framework.response import Response
 from compile_server.app.serializers import (UserSerializer,
                                             GroupSerializer,
-                                            ResourceSerializer)
+                                            ResourceSerializer,
+                                            ExampleSerializer)
 
 from compile_server.app.models import Resource, Example
 
@@ -71,9 +72,16 @@ def example(request, name):
 
 
 def code_page(request, example_name):
-    context = {'example_name': example_name}
+    matches = Example.objects.filter(name=example_name)
+    if not matches:
+        return Response()
+
+    e = matches[0]
+    serializer = ExampleSerializer(e)
+    context = {'example': serializer.data}
     return render(request, 'code_page.html', context)
 
+
 def examples_list(request):
     context = {'examples': Example.objects.all}
     return render(request, 'examples_list.html', context)

design/notes.txt

@@ -33,3 +33,17 @@ curl -H 'Accept: application/json; indent=4' http://127.0.0.1:8000/check_program
 
 # get the examples
 curl -H 'Accept: application/json; indent=4' http://127.0.0.1:8000/examples/ --header "Content-Type:application/json"
+
+#############################
+# Import Yannick's examples #
+#############################
+
+# TODO: add a facility to do this
+
+# Setup:
+cd resources ; git clone https:AdaCore/Compile_And_Prove_Demo.git
+
+# Import:
+./manage.py fill_examples --remove_all
+list="hello_world absolute_value bitwise_swap saturate_angle sensor_average strings communications landing_procedure"
+for a in $list; do ./manage.py fill_examples --dir=resources/Compile_And_Prove_Demo/examples/$a ; done