Fix early reporting of FV prover's output

This commit is contained in:
Hadrien Croubois
2023-05-04 10:20:40 +02:00
parent a7ee03565b
commit 2a6ccebfb7

View File

@ -75,13 +75,16 @@ async function runCertora(spec, contract, files, options = []) {
// as soon as we have a jobStatus link, print it
stream.on('data', function logStatusUrl(data) {
const urls = data.toString('utf8').match(/https?:\S*/g);
for (const url of urls ?? []) {
if (url.includes('/jobStatus/')) {
console.error(`[${spec}] ${url.replace('/jobStatus/', '/output/')}`);
const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
data
.toString('utf8')
.match(/-D\S+=\S+/g)
?.map(s => s.split('=')) || [],
);
if (jobId && userId) {
console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`);
stream.off('data', logStatusUrl);
break;
}
}
});
@ -98,7 +101,7 @@ async function runCertora(spec, contract, files, options = []) {
stream.end();
// write results in markdown format
writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)?.[0]);
writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
// write all details
console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));