[Termtools] Fwd: Re: TermComp'15 registration

Akihisa Yamada akihisa.yamada at uibk.ac.at
Fri Jul 3 09:32:30 CEST 2015


Dear Matthias and others,

it seems that I failed to send a mail concerning getting your tool
run on StarExec. I think some information below may help you...

> - Don't forget to do the same for backend solvers. For z3, it means
>   to edit "path-to-z3/build/config.mk" to have the following line:
>   "LINK_FLAGS=-static"

After that please re-link z3: remove the binary and "make".

Best regards,
Akihisa

-------- Forwarded Message --------
Subject: Re: [Termtools] TermComp'15 registration
Date: Thu, 2 Jul 2015 14:43:35 +0200
From: Akihisa Yamada <akihisa.yamada at uibk.ac.at>
To: Johannes Waldmann <johannes.waldmann at htwk-leipzig.de>, termtools 
<termtools at lri.fr>

Dear tool authors,

I'd like to share what I had to figure out in order to get my tool
run on StarExec.

(Some might contradict with what is written in StarExec User's Guide
  or elsewhere. It might be me who is wrong but please forgive me not
  having energy left to investigate further...)

- Don't use Google Chrome. It timeouts too quickly.

- Put configurations, i.e., scripts named "starexec_run_*", in "bin"
   directory in your archive.

- You can manually add and delete configurations later. But uploading
   and editing doesn't seem to work.

- Tool binaries cannot be updated. You have to upload a new solver.
   Of course this will discard configurations that are manually added,
   and you'll get a new set of IDs.

- Link statically. glibc on the server seems to be somewhat old
   (at least compared to my Ubuntu).

- For OCaml this means linking with "ocamlopt -cclib '-static'"

- Don't forget to do the same for backend solvers. For z3, it means
   to edit "path-to-z3/build/config.mk" to have the following line:
   "LINK_FLAGS=-static"

- Scripts seem to be invoked from somewhere unexpected, and you don't
   seem to have permission to write a file there. If you want to do so,
   you might want to use the directory where the script is, i.e.,
   "${0%/*}" in bash.

- You don't have $PATH to your tool binary. Call it using "${0%/*}" as
   well.

Best regards,
Akihisa

On 2015/07/01 13:36, Johannes Waldmann wrote:
> Dear all,
>
> I updated the web page with the registration information
> for this year's Termination Competition
>
> http://termination-portal.org/wiki/Termination_Competition_2015_Registration
>
> The process is the same as it was last year.
>
> If you are a competitor who takes part for the first time:
> Welcome!
>
> Do ask technical questions ("how do I do X")
> on this mailing list here (not email to me).
> Others - please help answering. Copy the answer to the list,
> to avoid duplicate effort. If applicable: write, extend,
> improve the corresponding Wiki page and post a link here.
>
> Best regards, Johannes.
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>

-- 
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/




More information about the Termtools mailing list