Merge pull request #2 from setton/master

Initial revision of checker

REQUIREMENTS.txt

@@ -1,2 +1,3 @@
 django
 djangorestframework
+pyyaml

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

@@ -7,6 +7,9 @@ from django.core.management.base import BaseCommand
 
 from compile_server.app.models import Resource, Example
 
+included_extensions = ['.ads', '.adb']
+# The extensions for the files that we want to show in the examples
+
 
 class Command(BaseCommand):
 
@@ -26,7 +29,7 @@ class Command(BaseCommand):
             Example.objects.all().delete()
 
         if options.get('dir', None):
-            d = options.get('dir')[0]
+            d = os.path.abspath(options.get('dir')[0])
 
             # For now, consider all files in the directory to be part of the
             # example
@@ -56,13 +59,15 @@ class Command(BaseCommand):
 
             resources = []
             for file in glob.glob(os.path.join(d, '*')):
-                with open(file, 'rB') as f:
-                    r = Resource(basename=os.path.basename(file),
-                                 contents=f.read())
-                    r.save()
-                    resources.append(r)
+                if any([file.endswith(ext) for ext in included_extensions]):
+                    with open(file, 'rB') as f:
+                        r = Resource(basename=os.path.basename(file),
+                                     contents=f.read())
+                        r.save()
+                        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,3 +1,37 @@
+// Launch a check on the given example editor
+function query_check_result(example_name, editors, container) {
+
+   files = []
+
+   editors.forEach(function(e){
+       files.push({'basename': e.basename,
+                   'contents': e.getValue()})
+   })
+
+   data = {"example_name": example_name,
+           "files": files}
+
+   // request the examples
+   $.ajax({
+      url: "/check_program/",
+      data: JSON.stringify(data),
+      type: "POST",
+      dataType : "json",
+      contentType: 'application/json; charset=UTF-8',
+   })
+   .done(function( json ) {
+      alert(json)
+   })
+   .fail(function( xhr, status, errorThrown ) {
+     //
+     alert( "could not run the example" );
+     console.log( "Error: " + errorThrown );
+     console.log( "Status: " + status );
+     console.dir( xhr );
+   })
+}
+
+
 // Fills a <div> with an editable representation of an example.
 //    container: the <div> in question
 //    example_name: the name of the example to load
@@ -66,9 +100,10 @@ function fill_editor(container, example_name) {
           editor.session.setMode("ace/mode/ada");
 
           // ... and their contents
-          editor.insert(resource.contents)
+          editor.setValue(resource.contents)
+          editor.gotoLine(1)
           editor.initial_contents = resource.contents
-          editor.filename = resource.basename
+          editor.basename = resource.basename
 
           // TODO: place the cursor at 1,1
 
@@ -84,13 +119,14 @@ function fill_editor(container, example_name) {
       reset_button.on('click', function (x){
           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){
-         alert(check_button.editors[1].filename)
+         query_check_result(example_name, check_button.editors, container)
       })
    })
    .fail(function( xhr, status, errorThrown ) {

compile_server/app/templates/code_page.html

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

compile_server/app/templates/examples_list.html

@@ -0,0 +1,16 @@
+{% extends 'base.html' %}
+{% block content %}
+
+{% for e in examples %}
+   <h3>{{ e.name }}</h3>
+
+   <div class="row">
+      <div class="col-md-8">
+         {{ e.description }}
+      </div>
+      <div class="col-md-4">
+         <a href="/code_page/{{ e.name }}" class="btn btn-primary btn-lg" role="button" aria-pressed="true">Go</a>
+      </div>
+    </div>
+{% endfor %}
+{% 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
 
@@ -40,15 +41,6 @@ class ResourceSet(viewsets.ModelViewSet):
     serializer_class = ResourceSerializer
 
 
-@api_view(['POST'])
-def check_program(request):
-    received_json = json.loads(request.body)
-    p = Program(code=received_json['program'])
-    serializer = ProgramSerializer(p)
-
-    return Response(serializer.data)
-
-
 @api_view(['GET'])
 def examples(request):
     """Return a list of example names and their description"""
@@ -80,6 +72,16 @@ def example(request, name):
 
 
 def code_page(request, example_name):
-    # TODO: move to a separate file
-    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)

compile_server/urls.py

@@ -18,20 +18,19 @@ from django.contrib import admin
 
 from rest_framework import routers
 
-from compile_server.app import views
+from compile_server.app import views, checker
 
 router = routers.DefaultRouter()
 router.register(r'users', views.UserViewSet)
 router.register(r'groups', views.GroupViewSet)
 
 urlpatterns = [
-    url(r'^', include(router.urls)),
     url(r'^api-auth/', include('rest_framework.urls',
                                namespace='rest_framework')),
     url(r'^admin/', admin.site.urls),
 
     # Check one program
-    url(r'^check_program/', views.check_program),
+    url(r'^check_program/', checker.check_program),
 
     # Get a list of the examples
     url(r'^examples/', views.examples),
@@ -44,4 +43,9 @@ urlpatterns = [
     # Get the code viewer on one example
     url(r'^code_page/([^\/]+)$', views.code_page),
 
+    # Get a list of all the examples
+    url(r'^examples_list/', views.examples_list),
+
+    # The landing page
+    url(r'', views.examples_list),
 ]

design/notes.txt

@@ -9,7 +9,6 @@ Notes just for myself
 
 Frontend
 
-* fix selection after clicking the "reset" button
 * nicer display when an example was not found
 * grab the bits that are currently served by CDNs
 
@@ -17,7 +16,6 @@ Backend
 
 * cleanup the status of imported/invisible files (exclude yaml, project)
 * implement the "check" button
-* implement a page which lists all the examples
 
 Production
 
@@ -35,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