Mentions légales du service

Skip to content

Use floats for timelimits

Xavier Denis requested to merge fractional-limits into master

This implements the first half of #737 (closed) by using float everywhere for timelimits.

I'm making this so I can see if CI breaks (it shouldn't).

I think the biggest thing that is missing is ensuring that we also parse 5 in the various inputs (config, transformations in the ide).

TODO:

  • Add a new %T for prover commands that support floating point time limits. I'm not clear how the substitution actually substitution happens though.
Edited by Xavier Denis

Merge request reports