Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Nov 05, 2014 at 09:14:47PM +0000, Jason Gross wrote:
> Hi,
> I've noticed that ssreflect has many pretty timing graphs, and I'd like to
> generate similar ones for HoTT/HoTT.  I have a few questions:
> (1) Is it permissible for me to copy over some of the graph-building
> scripts from ssr to HoTT, and, if so, what licence should I put at the top
> of them, or what should I add to our licence file?

I'm attaching an archive with all the scripts, but I don't think you
should copy them.  Recent jenkins versions have plugins to store and
plot timings.  I've never studied them, but they are likely to be
simpler and more future proof that my bunch of shell/lua/sed scripts.

The json2*.lua files drive gnuplot (you need luajson and luafilesystem
to run them).  I guess rewriting them in python or any other language
is a good option if you are not familiar with Lua.  The builssr script
generates a csv file, that is then turned into a json one (I don't
recall why), then it is archived in a place known by the plotting
scripts.

The timeout script is not work of mine, and has its own license.

The build-strub-contrib.sh script is by Pierre-Yves Strub, but I don't
think you really need it.  If you do, ask him.

The other files are work of mine, let say they are under the Expat
license (3 clauses BSD).

IMO, the only valuable data are the gnuplot "templates" (the json2*.lua
scipts).  But for that, it is probably quicker to rewrite things than to
understand the code I wrote.
The main idea of the shell scripts, write down an environ file that one
can "continue" a job, is something you already know (also in the windows
SDK you contributed to).

> (2) Would it be possible to get a copy of the jenkins configuration for
> ssr, so I could see what scripts are being called and with what arguments?

The typical job does:
 - svn update /srv/scripts
 - /srv/scripts/buildsomething coq-branch

Good luck,
-- 
Enrico Tassi

Attachment: jenins.zip
Description: Zip archive