Add repository premium flag and lots of fixes

.travis.yml

@@ -1,3 +1,5 @@
+dist: trusty
+sudo: required
 language: ruby
 
 rvm:
@@ -8,6 +10,11 @@ cache:
 
 addons:
   postgresql: '9.3'
+  apt:
+    sources:
+      - elasticsearch-2.x
+    packages:
+    - elasticsearch
 
 branches:
   except:
@@ -44,7 +51,9 @@ before_script:
   - sudo apt-add-repository -y 'deb http://archive.canonical.com/ubuntu precise partner'
   - sudo apt-add-repository -y 'deb http://archive.ubuntu.com/ubuntu precise-updates main restricted universe multiverse'
   - sudo apt-get update
-  - sudo apt-get install libsane libgphoto2-2 hets-core subversion udrawgraph git-svn
-  - sudo hets -update
+  - sudo apt-get install libsane libgphoto2-2 hets-server subversion git-svn
+  - sudo ln -s /usr/bin/hets-server /usr/bin/hets
+  - sudo ln -s /usr/lib/hets/hets-server /usr/lib/hets/hets
   - mkdir -p tmp/{git,data/{git,git_daemon,commits}}
+  - curl http://localhost:9200
   - RAILS_ENV=test bundle exec rake db:migrate || true

app/assets/stylesheets/data_type.css.sass

@@ -21,7 +21,6 @@
     position:  -4px center !important
   padding-left: 30px !important
 
-
 .ui-autocomplete a, .relationList li, a
   &[data-type=Team]
     +data-icon(team)

app/assets/stylesheets/proof.css.sass

@@ -9,10 +9,10 @@
 .columnized-items
   div.form-group div.col-lg-10
     > label
-      @extend .col-lg-2
-      @extend .col-md-3
-      @extend .col-sm-4
-      @extend .col-xs-6
+      @extend .col-lg-4
+      @extend .col-md-6
+      @extend .col-sm-12
+      @extend .col-xs-12
       margin: 0
       float: left
     > p.help-block

app/controllers/home_controller.rb

@@ -7,7 +7,9 @@ def index
     @comments = Comment.latest.limit(10)
     @versions = OntologyVersion.accessible_by(current_user).latest.
       where(state: 'done').limit(10)
-    @repositories = Repository.accessible_by(current_user).latest.limit(10)
+    @repositories = Repository.accessible_by(current_user).latest
+    @featured_repositories = @repositories.where(featured: true).limit(10)
+    @common_repositories = @repositories.where(featured: false).limit(10)
   end
 
   def show

app/controllers/repositories_controller.rb

@@ -23,7 +23,9 @@ def update
   end
 
   def index
-    @repositories = Repository.accessible_by(current_user)
+    @repositories = Repository.accessible_by(current_user).order(:path)
+    @featured_repositories = @repositories.where(featured: true)
+    @common_repositories = @repositories.where(featured: false)
     super
   end
 

app/fake_records/repository_file.rb

@@ -199,7 +199,12 @@ def initialize_for_create_and_update(opts)
       @target_filename  = opts[:path].split('/')[-1]
     else
       @target_directory = opts[:target_directory]
-      @target_filename  = opts[:target_filename]
+      @target_filename  =
+        if opts[:target_filename].blank? && opts[:temp_file].present?
+          opts[:temp_file].headers.match(/filename="([^"]+)"/)[1]
+        else
+          opts[:target_filename]
+        end
     end
     @temp_file  = opts[:temp_file]
     @file_upload_type = opts[:file_upload_type]
@@ -234,4 +239,3 @@ def prepare_opts_on_file_upload(opts)
   end
 
 end
-

app/helpers/link_helper.rb

@@ -28,9 +28,15 @@ def fancy_link(resource)
         resource
       end
 
-    link_to name, linked_to,
+    link = link_to name, linked_to,
       data_type => value,
       title: title
+
+    if resource.respond_to?(:featured?) && resource.featured?
+      %(<i class="fa fa-star-o"></i> #{link}).html_safe
+    else
+      link
+    end
   end
 
   def format_links(*args, &block)

app/models/ability.rb

@@ -38,6 +38,9 @@ def initialize(user, access_token)
           (subject.permission?(:editor, user) || subject.public_rw?)
         end
       end
+      can [:feature], Repository do |subject|
+        user.admin?
+      end
       can [:update, :destroy, :permissions], Repository do |subject|
         subject.permission?(:owner, user)
       end

app/models/axiom_selection.rb

@@ -6,6 +6,7 @@ class AxiomSelection < ActiveRecord::Base
   attr_accessible :finished
 
   has_many :proof_attempt_configurations, dependent: :destroy
+  has_many :proof_attempts, through: :proof_attempt_configurations
   has_and_belongs_to_many :axioms,
                           class_name: 'Axiom',
                           association_foreign_key: 'sentence_id',

app/models/hets_instance.rb

@@ -9,10 +9,7 @@ def initialize(msg = DEFAULT_MSG)
   end
 
   class NoSelectableHetsInstanceError < Error
-    DEFAULT_MSG = <<-MSG
-There is no HetsInstance which is reachable and
-has a minimal Hets version of #{Hets.minimal_version_string}
-    MSG
+    DEFAULT_MSG = 'There is no HetsInstance which is reachable'
 
     def initialize(msg = DEFAULT_MSG)
       super
@@ -34,7 +31,7 @@ def initialize(msg = DEFAULT_MSG)
   validate :queue_size, numericality: {greater_than_or_equal_to: 0}
 
   scope :active, -> do
-    where(up: true).where('version >= ?', Hets.minimal_version_string)
+    where(up: true)
   end
   scope :free, -> do
     where(state: 'free')

app/models/manual_axiom_selection.rb

@@ -1,3 +1,4 @@
 class ManualAxiomSelection < ActiveRecord::Base
   acts_as :axiom_selection
+  has_many :proof_attempts, through: :axiom_selection
 end

app/models/ontology/associations_and_attributes.rb

@@ -14,6 +14,8 @@ module Ontology::AssociationsAndAttributes
     belongs_to :repository
     belongs_to :formality_level
 
+    has_one :loc_id, foreign_key: :specific_id
+
     has_many :symbol_groups
     has_many :alternative_iris, dependent: :destroy
     has_many :source_mappings,

app/models/ontology/hets_options.rb

@@ -3,7 +3,7 @@ module Ontology::HetsOptions
 
   # Hets has some trouble inferring those input types
   # by itself, so we give it a hint:
-  EXTENSIONS_TO_INPUT_TYPES = {'.p' => 'tptp'}
+  EXTENSIONS_TO_INPUT_TYPES = {'.ax' => 'tptp', '.p' => 'tptp'}
 
   def hets_options
     Hets::HetsOptions.new(:'url-catalog' => repository.url_maps,

app/models/ontology/mappings.rb

@@ -26,13 +26,37 @@ def determine_mapping_type(typename)
         kind || Mapping::DEFAULT_MAPPING_KIND
       end
 
+      def determine_mapping_endpoint_iri(endpoint_iri, endpoint)
+        return endpoint_iri if endpoint_iri
+        absolute =
+          begin
+            URI(endpoint).absolute?
+          rescue ArgumentError
+            false
+          end
+        owner = proxy_association.owner
+        if owner.distributed?
+          locid_for_child(endpoint)
+        elsif owner.locid.end_with?(endpoint)
+          # It's a mapping to this single ontology - a locid for a child would
+          # be wrong. The IRI must point to this single ontology:
+          "#{Hostname.url_authority}#{owner.locid}"
+        elsif absolute
+          endpoint
+        else
+          # It's a mapping to a single ontology - a locid for a child would be
+          # wrong. Guess that the endpoint is in the repository root:
+          "#{Hostname.url_authority}/#{owner.repository.path}/#{endpoint}"
+        end
+      end
+
       def update_or_create_from_hash(hash, _user, timestamp = Time.now)
         raise ArgumentError, 'No hash given.' unless hash.is_a? Hash
         # hash['name'] # maybe nil, in this case, we need to generate a name
         mapping_iri   = locid_for_child(hash['name'] || hash['linkid'])
         mapping_name  = hash['name']
-        source_iri = hash['source_iri'] || locid_for_child(hash['source'])
-        target_iri = hash['target_iri'] || locid_for_child(hash['target'])
+        source_iri = determine_mapping_endpoint_iri(hash['source_iri'], hash['source'])
+        target_iri = determine_mapping_endpoint_iri(hash['target_iri'], hash['target'])
 
         source = Ontology.find_with_iri(source_iri) || (raise ArgumentError,
           "source #{Settings.OMS} not found: #{source_iri}")

app/models/proof_status.rb

@@ -7,6 +7,7 @@ class ProofStatus < ActiveRecord::Base
   DEFAULT_DISPROVEN_STATUS = 'CSA'
   DEFAULT_DISPROVEN_ON_SUBSET = 'CSAS'
   DEFAULT_UNKNOWN_STATUS = 'UNK'
+  DEFAULT_TIMEOUT_STATUS = 'TMO'
   CONTRADICTORY = 'CONTR'
 
   self.primary_key = :identifier

app/models/repository/associations_and_attributes.rb

@@ -14,6 +14,7 @@ module Repository::AssociationsAndAttributes
                       :source_address,
                       :remote_type,
                       :access,
+                      :featured,
                       :destroy_job_id,
                       :is_destroying
   end

app/models/sine_axiom_selection.rb

@@ -12,6 +12,7 @@ class SineAxiomSelection < ActiveRecord::Base
   attr_accessible :commonness_threshold, :depth_limit, :tolerance
   has_many :sine_symbol_commonnesses, dependent: :destroy
   has_many :sine_symbol_axiom_triggers, dependent: :destroy
+  has_many :proof_attempts, through: :axiom_selection
 
   validates_numericality_of :commonness_threshold,
                             greater_than_or_equal_to: 0,
@@ -117,6 +118,7 @@ def other_finished_sine_axiom_selections
   def select_axioms
     @selected_axioms = triggered_axioms_by_commonness_threshold.to_a
     select_new_axioms(goal, 0)
+    @selected_axioms += select_exceptions
     self.axioms = @selected_axioms.uniq
   end
 
@@ -152,4 +154,38 @@ def depth_limit_reached?(current_depth)
   def depth_limited?
     depth_limit != -1
   end
+
+  def select_exceptions
+    return [] unless tptp?
+    # Select all type formulae of TFF/THF
+    all_type_and_definition_sentences = goal.ontology.sentences.
+      where("text ILIKE 'tff(%,%type%,%' OR text ILIKE 'thf(%,%type%,%' OR text ILIKE 'tff(%,%definition%,%' OR text ILIKE 'thf(%,%definition%,%'")
+
+    selected_symbol_ids =
+      @selected_axioms.map { |sen| sen.symbols.select(:id) }.flatten.uniq
+
+    additional_axioms = []
+    new_axioms = [:just_a_start_value_which_is_deleted_in_the_next_step]
+    while new_axioms.nil? || new_axioms.any?
+      new_axioms = select_exceptions_types_defs(all_type_and_definition_sentences,
+                                                selected_symbol_ids)
+      selected_symbol_ids = new_axioms.map { |sen| sen.symbols.select(:id) }.flatten.uniq
+      new_axioms -= additional_axioms
+      additional_axioms += new_axioms
+      puts new_axioms.map(&:id)
+    end
+    additional_axioms
+  end
+
+  def select_exceptions_types_defs(all_type_and_definition_sentences, selected_symbol_ids)
+    all_type_and_definition_sentences.select do |sentence|
+      sentence.symbols.select(:id).any? do |sentence_symbol_id|
+        selected_symbol_ids.include?(sentence_symbol_id)
+      end
+    end
+  end
+
+  def tptp?
+    goal.ontology.logic.name.downcase == 'tptp'
+  end
 end

app/views/home/_versions.html.haml

@@ -3,10 +3,19 @@
 .pull-right
   = link_to 'Browse Repositories', repositories_path, class: 'btn btn-primary', type: 'button'
 
-- @repositories.each do |repository|
-  %div
-    = fancy_link repository
-    = timestamp repository.updated_at
+- if @featured_repositories.any?
+  %h4 Featured
+  - @featured_repositories.each do |repository|
+    %div
+      = fancy_link repository
+      = timestamp repository.updated_at
+
+- if @common_repositories.any?
+  %h4 Common
+  - @common_repositories.each do |repository|
+    %div
+      = fancy_link repository
+      = timestamp repository.updated_at
 
 %h2 Recently Updated #{Settings.OMS.pluralize.capitalize}
 

app/views/repositories/_form.html.haml

@@ -20,4 +20,8 @@
     = select_tag :access_options_non_mirror, options_for_select(access_options)
     = select_tag :access_options_mirror, options_for_select(access_options_mirror)
 
+  - if can?(:feature, @repository)
+    = f.input :featured, as: :boolean
+
+
   = f.button :wrapped

app/views/repositories/index.html.haml

@@ -15,7 +15,16 @@
       = t('.clone_list_prefix')
       = link_to t('.clone_list_link'), repositories_path(format: :txt)
 
-.row
-  .col-md-12.repository-index
-    %ul.list-group
-      = render collection
+- if @featured_repositories.any?
+  %h3 Featured Repositories
+  .row
+    .col-md-12.repository-index
+      %ul.list-group
+        = render @featured_repositories
+
+- if @common_repositories.any?
+  %h3 Common Repositories
+  .row
+    .col-md-12.repository-index
+      %ul.list-group
+        = render @common_repositories

config/database.yml

@@ -5,7 +5,7 @@ development: &config
   adapter: postgresql
   encoding: unicode
   template: template0
-  database: ontohub_development
+  database: ontohub_legacy_development
   username: postgres
   password:
   pool: 5
@@ -30,7 +30,7 @@ development: &config
 # Do not set this db to the same as development or production.
 test: &test
   <<: *config
-  database: ontohub_test
+  database: ontohub_legacy_test
 
 production:
   <<: *config

config/locales/en.yml

@@ -162,8 +162,8 @@ en:
   proofs:
     new:
       title: 'Attempt to prove %{klass} %{resource}'
-      theorems_definitions: Definitions
-      theorem_definition: Definition
+      theorems_definitions: Theorems to prove
+      theorem_definition: Theorem to prove
       configuration: Proving Configuration
       send: 'Prove'
       klass:

db/migrate/20170222120000_add_ax_to_file_extensions.rb

@@ -0,0 +1,29 @@
+class AddAxToFileExtensions < ActiveRecord::Migration
+  def up
+    populate_database_with_ontology_file_extensions
+    populate_database_with_file_extension_mime_type_mappings
+  end
+
+  def populate_database_with_ontology_file_extensions
+    file_extensions_single = %w[ax p]
+    file_extensions_single.map! { |e| ".#{e}" }
+    file_extensions_single.each do |ext|
+      ActiveRecord::Base.connection.execute(
+        "INSERT INTO ontology_file_extensions (extension, distributed) VALUES ('#{ext}', 'false')")
+    end
+  end
+
+  def populate_database_with_file_extension_mime_type_mappings
+    mappings = [
+      %w(.ax text/tptp),
+      %w(.p text/tptp),
+      %w(.tptp text/tptp),
+    ]
+
+    mappings.each do |(file_extension, mime_type)|
+      FileExtensionMimeTypeMapping.
+        where(file_extension: file_extension, mime_type: mime_type).
+        first_or_create!
+    end
+  end
+end