Stream: Coq devs & plugin devs

Topic: Windows build issue


view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:18):

Someone changed the password for two of the 7 servers - I can't clean them up and I fear these are the ones causing trouble. The others where fairly clean, although there seems to be some new problem with cygwin registering fonts, and these fonts then canot be deleted unless one unregisters them. But the data size is small. None of teh 5 servers I cleand was above 75% and if they are clean they are about 70% (which is occupied by the OS).

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:19):

The servers with changed password are: coq-windows and coq-windows-untrusted2

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:22):

The servers with changed password are: coq-windows and coq-windows-untrusted2

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:22):

I can at least disable these runners from the GitLab settings.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:25):

@Théo Zimmermann : yes, please remove these and try to find out who did this. Btw.: How do I quote on Zulip?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:25):

Michael Soegtrop said:

Théo Zimmermann : yes, please remove these and try to find out who did this. Btw.: How do I quote on Zulip?

You can quote a full message by going on the down arrow sign when hovering over a message.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:26):

Or you can use standard Markdown syntax to quote part of a message, i.e.:

> quote

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:29):

@Michael Soegtrop I realize that the failure actually happened on this runner: coq-windows-untrusted-i01

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:30):

See the log: https://gitlab.com/coq/coq/-/jobs/580779004

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:31):

Michael Soegtrop I realize that the failure actually happened on this runner: coq-windows-untrusted-i01

This one I cleaned and it didn't look bad (75% pre clean, which is good enough, it starts to get critical beyond 90%)

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:34):

@Théo Zimmermann : the log says:

               8 Dir(s)  12�376�797�184 bytes free
Install cygwin and download, compile and install OCaml and Coq for MinGW
 Illegal parameter REM

Looks like someone is feeding the build script with bad parameters. 12 GB free is good enough.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:36):

OK sorry, then it is my fault.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:36):

I thought REM was the way to comment out stuff in batch scripts.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:37):

(FTR, I've split out the two discussions in separate topics to avoid having them interleave)

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:37):

Théo Zimmermann said:

I thought REM was the way to comment out stuff in batch scripts.

maybe a dangling nd of line quote - REM works only at the beginnong of a line (originally it was a command which does nothing)

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:37):

End of line quoting as in sh does not work in batchfiles

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:38):

See https://github.com/coq/coq/pull/12415/files#diff-0cdf0025903e08b0d7118360b8b60743, can you tell me what is the issue?

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:39):

    -addon=coquelicot ^
    -addon=vst ^
REM    -addon=vst ^
    -addon=aactactics ^

A dnagling end of line quote - the ^ is DOS' line continuation character so you have a REM in the middle of a SET command. This does not work.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:40):

I usually move the commented out lines below

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 09:40):

OK thanks!

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 09:41):

Btw.: I think even in sh this wouldn't work since it would comment out the remaining entries

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:31):

@Théo Zimmermann : can you please try to find out how changed the password on the two runners - usually we need them most close to a release. Or have someone who has admin access reset the passwords.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:34):

@Maxime Dénès Do you have any idea about this?

view this post on Zulip Maxime Dénès (Jun 04 2020 at 10:40):

Sounds strange. I didn't change the password. Who else could've done it?

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:42):

@Maxime Dénès : in case you have the Administraor password, please just set the password of user CI to what it was.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 21:32):

@Maxime Dénès @Théo Zimmermann I checked again and I can login into the two runners again. I guess you did reset the password?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 21:33):

I didn't do anything.

view this post on Zulip Maxime Dénès (Jun 04 2020 at 22:25):

I haven't yet. The plot thickens!


Last updated: Oct 15 2021 at 19:03 UTC