From 2a6ccebfb7a7c080ef8bcf547115b65731665ba2 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 4 May 2023 10:20:40 +0200 Subject: [PATCH 1/2] Fix early reporting of FV prover's output --- certora/run.js | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/certora/run.js b/certora/run.js index 2dc7d0181..24a676d94 100755 --- a/certora/run.js +++ b/certora/run.js @@ -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/')}`); - stream.off('data', logStatusUrl); - break; - } + 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); } }); @@ -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)); From 7c37ea0ff677b916acfefe7b3c4fd7531ddc4ae2 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 4 May 2023 10:23:59 +0200 Subject: [PATCH 2/2] fix rewrite --- certora/run.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/run.js b/certora/run.js index 24a676d94..3fb2c6c56 100755 --- a/certora/run.js +++ b/certora/run.js @@ -139,8 +139,8 @@ function writeEntry(spec, contract, success, url) { spec, contract, success ? ':x:' : ':heavy_check_mark:', + url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error', url ? `[link](${url})` : 'error', - url ? `[link](${url?.replace('/jobStatus/', '/output/')})` : 'error', ), ); }