hets.rb revision fb2c319c7cce96c35e06be8fe6f60da7d040c952
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield attr_reader :path, :library_path, :stack_size, :env, :yaml
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield yaml = YAML.load_file(File.join(Rails.root, 'config', 'hets.yml'))
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield @path = first_which_exists yaml['hets_path']
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield @library_path = first_which_exists yaml['hets_lib']
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield @stack_size = yaml['stack_size'] || '1G'
96283b546081e7ff709968378fca25cb44f1ab6cStéphane Graber raise Hets::DeploymentError, 'Could not find hets' unless @path
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield raise Hets::DeploymentError, 'Hets library not found.' unless @library_path
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield check_validity_of_version(yaml['version_minimum_revision'])
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # Set hets environment variables
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield %w( hets_lib hets_owl_tools ).each do |key|
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield @env[key.upcase] = first_which_exists yaml[key]
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield "v#{minimum_version}, #{minimum_revision}"
826cde7c2100e1f4419a54b5c930c0854e01e87eMichael H. Warfield # Checks Hets installation compatibility by its version date
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # * - +minimum_revision+ -> Minimum working hets version revision
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # * *Returns* :
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # * - true if hets version minimum revision smaller than or equal to actual hets version revision
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # * - false otherwise
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # Read Hets version minimum revision
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield raise ConfigDateFormatError, 'Could not read hets version minimum revision in YAML' unless minimum_revision
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # Read Hets version date
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield # revision starts with r-char and ends with revision number.
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield version_revision = if version =~ VERSION_RE
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield $1 # the version number (unix timestamp)
826cde7c2100e1f4419a54b5c930c0854e01e87eMichael H. Warfield raise InvalidHetsVersionFormatError, "format is not valid: <#{version}>"
826cde7c2100e1f4419a54b5c930c0854e01e87eMichael H. Warfield # Return true if minimum date is prior or equal to version date
b4f7af7a520b23c873e404562ec518a576e63d4cMichael H. Warfield return minimum_revision.to_i <= version_revision.to_i
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield paths.map { |path| File.expand_path path }.find do |path|
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield def check_validity_of_version(reference_version)
8ec981fc8b0105da5f071e40811e0c2472a6c3c9Stéphane Graber raise VersionOutdatedError, 'The installed version of Hets is too old'
8ec981fc8b0105da5f071e40811e0c2472a6c3c9Stéphane GraberThe Hets Version identifier was not recognized
8ec981fc8b0105da5f071e40811e0c2472a6c3c9Stéphane Graber(#{e.message}),
8ec981fc8b0105da5f071e40811e0c2472a6c3c9Stéphane Graberwe expected it to be matchable by this regular expression:
8ec981fc8b0105da5f071e40811e0c2472a6c3c9Stéphane Graber#{VERSION_RE}.
207bf0e475f1dc6e9a2dac2cee3a209b56427855Stéphane Graber Rails.logger.warn message
207bf0e475f1dc6e9a2dac2cee3a209b56427855Stéphane Graber STDERR.puts message
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield def self.config
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield @config ||= Hets::Config.new
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield def self.minimal_version_string
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield config.minimal_version_string
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.minimum_revision
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield config.minimum_revision
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield def self.minimum_version
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield config.minimum_version
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.qualified_loc_id_for(resource)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield locid = URI.escape(resource.versioned_locid)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield "http://#{Settings.hostname}#{locid}"
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.parse_via_api(resource, hets_options, structure_only: false)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield mode = structure_only ? :fast_run : :default
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield parse_caller = Hets::ParseCaller.new(HetsInstance.choose!, hets_options)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield parse_caller.call(qualified_loc_id_for(resource), with_mode: mode)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.prove_via_api(resource, prove_options)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield prove_caller = Hets::ProveCaller.new(HetsInstance.choose!, prove_options)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield prove_caller.call(qualified_loc_id_for(resource))
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.provers_via_api(resource, provers_options)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield provers_caller = Hets::ProversCaller.new(HetsInstance.choose!, provers_options)
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield provers_caller.call(qualified_loc_id_for(resource))
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield def self.filetype(resource)
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield iri = qualified_loc_id_for(resource)
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield filetype_caller = Hets::FiletypeCaller.new(HetsInstance.choose!)
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield response_iri, filetype = filetype_caller.call(iri).split(': ')
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield if response_iri == iri
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield Mime::Type.lookup(filetype)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield raise FiletypeNotDeterminedError.new("#{response_iri}: #{filetype}")
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # Runs hets with input_file and returns XML output file path.
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.parse(input_file, url_catalog = [], output_path = nil, structure_only: false)
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # Arguments to run the subprocess
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args = [config.path, *%w( -o pp.xml -o xml --full-signatures -a none -v2 --full-theories )]
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield if output_path
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield FileUtils.mkdir_p output_path
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args += ['-O', output_path]
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args += ['-s'] if structure_only
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args += ['-C', url_catalog.join(',')] unless url_catalog.empty?
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # Configure stack size
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args += ['+RTS', "-K#{config.stack_size}", '-RTS']
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # add the path to the input file as last argument
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield args << input_file
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # Executes command with low priority
17abf2784de1047fb2904ff130ee5efe4ea7b598Elan Ruusamäe Rails.logger.debug "Running hets with: #{args.inspect}"
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield output = Subprocess.run :nice, *args, config.env
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield if output.starts_with? '*** Error'
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # some error occured
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield raise ExecutionError, output
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield elsif (files = written_files(output.lines)).any?
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # successful execution
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield # we can not handle this response
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield raise ExecutionError, "Unexpected output:\n#{output}"
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield rescue Subprocess::Error => e
164105f6563d98b832f603e28e506dbabed22cf3Michael H. Warfield output = e.output
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield # Exclude usage message if exit status equals 2
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield if e.status == 2 and output.include? 'Usage:'
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield raise ExecutionError, output.split("Usage:").first
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield raise ExecutionError, e.message
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.config
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield @@config ||= Config.new
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.written_files(lines)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield lines.reduce([]) do |lines, line|
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield file = written_file(line)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield lines << file if file
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield def self.written_file(line)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield match = line.match(/Writing file: (?<file>.+)/)
c6df5ca4603c630a7189cdb1653c96bd2808c7e5Michael H. Warfield match[:file] if match