Byla vydána pro lidi zdarma ke stažení kniha The Book of Remind věnovaná sofistikovanému kalendáři a připomínači Remind.
Grafický editor dokumentů LyX, založený na TeXu, byl vydán ve verzi 2.5.0. Oznámení připomíná 30. výročí vzniku projektu. Novinky zahrnují mj. vylepšení referencí nebo použití barev napříč aplikací, od rozhraní editoru po výstupní dokument.
F-Droid bannerem na svých stránkách a také v aplikacích F-Droid a F-Droid Basic upozorňuje na iniciativu Keep Android Open. Od září 2026 bude Android vyžadovat, aby všechny aplikace byly registrovány ověřenými vývojáři, aby mohly být nainstalovány na certifikovaných zařízeních Android. To ohrožuje alternativní obchody s aplikacemi jako F-Droid a možnost instalace aplikací mimo oficiální obchod (sideloading).
Svobodná historická realtimová strategie 0 A.D. (Wikipedie) byla vydána ve verzi 28 (0.28.0). Její kódový název je Boiorix. Představení novinek v poznámkách k vydání. Ke stažení také na Flathubu a Snapcraftu.
Multimediální server a user space API PipeWire (Wikipedie) poskytující PulseAudio, JACK, ALSA a GStreamer rozhraní byl vydán ve verzi 1.6.0 (Bluesky). Přehled novinek na GitLabu.
UBports, nadace a komunita kolem Ubuntu pro telefony a tablety Ubuntu Touch, vydala Ubuntu Touch 24.04-1.2 a 20.04 OTA-12.
Byla vydána (Mastodon, 𝕏) nová stabilní verze 2.0 otevřeného operačního systému pro chytré hodinky AsteroidOS (Wikipedie). Přehled novinek v oznámení o vydání a na YouTube.
WoWee je open-source klient pro MMORPG hru World of Warcraft, kompatibilní se základní verzí a rozšířeními The Burning Crusade a Wrath of the Lich King. Klient je napsaný v C++ a využívá vlastní OpenGL renderer, pro provoz vyžaduje modely, grafiku, hudbu, zvuky a další assety z originální kopie hry od Blizzardu. Zdrojový kód je na GitHubu, dostupný pod licencí MIT.
Byl představen ICT Supply Chain Security Toolbox, společný nezávazný rámec EU pro posuzování a snižování kybernetických bezpečnostních rizik v ICT dodavatelských řetězcích. Toolbox identifikuje možné rizikové scénáře ovlivňující ICT dodavatelské řetězce a na jejich podkladě nabízí koordinovaná doporučení k hodnocení a mitigaci rizik. Doporučení se dotýkají mj. podpory multi-vendor strategií a snižování závislostí na vysoce
… více »Nizozemský ministr obrany Gijs Tuinman prohlásil, že je možné stíhací letouny F-35 'jailbreaknout stejně jako iPhony', tedy upravit jejich software bez souhlasu USA nebo spolupráce s výrobcem Lockheed Martin. Tento výrok zazněl v rozhovoru na BNR Nieuwsradio, kde Tuinman naznačil, že evropské země by mohly potřebovat větší nezávislost na americké technologii. Jak by bylo jailbreak možné technicky provést pan ministr nijak nespecifikoval, nicméně je známé, že izraelské letectvo ve svých modifikovaných stíhačkách F-35 používá vlastní software.
17.2.2013 20:42
Bystroushaak | skóre: 36
| blog: Bystroushaakův blog
| Praha
Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
AbcLinuxu.cz
ITBiz.cz
HDmag.cz
AbcPráce.cz-- nejprve operator ekvivalence
(==) :: Eq a => a -> a -> Bool
-- nerovnost ?
(/=) ? Eq a => a -> a -> Bool
-- error: cannot infer
-- musi natukat clovek
x /= y == not (x == y)
-- a je to :)
x /= y = not (x == y)Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
Docela mě překvapuje, že to nevrátí třeba x /= y = True.
Příkaz Auto zvládne doplnit i složitější výrazy. Například return a bind pro stavovou monádu doplní takto:
record Pair (A B : Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B
record State (S A : Set) : Set where
constructor state
field
runState : S → Pair S A
-- vygenerovane prikazem Auto
return : {S A : Set} → A → State S A
return x = state (λ z → z , x)
-- vygenerovane prikazem Auto (a spatne)
bind : {S A B : Set} → State S A → (A → State S B) → State S B
bind m f = state
(λ z →
z ,
Pair.proj₂
(State.runState (f (Pair.proj₂ (State.runState m z))) z))
bind je bohužel špatně – typ totiž nezakazuje použití původního stavu. Když ale umožním, aby se typ stavu měnil (pak už to není monáda), tak Auto vygeneruje již korektní definici i pro bind:
record IState (S₁ S₂ A : Set) : Set where
constructor state
field
runState : S₁ → Pair S₂ A
-- vygenerovane prikazem Auto
ibind : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind m f = state
(λ z →
Pair.proj₁
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z)))
,
Pair.proj₂
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z))))
Nicméně perfektní to není – některé výrazy se tam zbytečně opakují, člověk by napsal:
-- napsane clovekem
ibind' : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind' m f = state
(λ st₁ →
let (st₂ , a) = IState.runState m st₁
in IState.runState (f a) st₂)
IMHO to ale moc prakticky neni.Hodí se to v důkazech. Tam potřebuji najít term s daným typem a už příliš nezáleží na tom, jak ten term vypadá.
18.2.2013 13:38
coder | skóre: 4
| blog: lINUKS
18.2.2013 21:00
Josef Kufner | skóre: 70
19.2.2013 15:28
coder | skóre: 4
| blog: lINUKS
Bez Vimu si jiz nedokazi predstavit svuj zivot 
Ale ten Emacs ma spousty zajimavych funkci a doplnku, ktere bych rad pouzival a ve svete vimu jsou nedokonale imitovane. Napr. org mod a velmi kvalitni integrace REPLu funkcionalnich jazyku. No uvidim, treba se nekdy hacknu.
Hm, moc tomu nerozumim
Máte nějaký konkrétní dotaz, třeba bych mohl pomoci?
Mně se na Agdě a podobných jazycích líbí minimalističnost kombinovaná se silou typového systému. Naopak mi vadí absence aktuální definice jazyka – bylo by super, kdyby někdo zpracoval definici na úrovni Standard ML (viz stará verze: The Definition of Standard ML - Version 2).
Hlavní využití příkazu Auto je při hledání důkazů – tam totiž jde pouze o nalezení termu s odpovídajícím typem a je jedno, jak ten term vypadá. Je tohle odpověď na vaši otázku?
int f(int a, int b)a editor me k tomu doplnil:
{
return a + b;
}
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
Přesně tak. Například, když chci odčítání a použiji typ
binop₁ : ℕ → ℕ → ℕ
tak dostanu
binop₁ a b = b
což není odčítání. Musím tedy upřesnit typ:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)
Místo pouhého čísla vracím dvojici. První prvek dvojice je číslo a druhý prvek je důkaz, že první prvek je rozdíl x a y. Odečítání definuji následovně:
_∸_ : ℕ → ℕ → ℕ m ∸ zero = m zero ∸ _ = zero suc m ∸ suc n = m ∸ n
Rovnost vyjadřuji pomocí následujícího typu. Typ je navržen tak, že term refl typu a ≡ b jde zkonstruovat pouze tehdy, jsou-li a a b stejné:
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
Následuje definice závislého páru, kde typ druhé složky závisí na hodnotě první složky:
record Pair (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
Nastavení parseru:
infixl 6 _∸_ infix 4 _≡_ _,_
Funkce vracející typ (tj. výrok), že rozdíl prvních dvou čísel je roven třetímu číslu:
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = x ∸ y ≡ res
Pro tento typ už příkaz Auto vygeneruje požadovanou funkci:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y) binop₂ a b = a ∸ b , refl
24.2.2013 22:50
Josef Kufner | skóre: 70
Myslím, že neuniká. V ničem to není lepší. Je to jen příklad, že vlastnost výsledku funkce jde specifikovat typem. V tomto případě to však nemá žádné výhody – spíše naopak.
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.
25.2.2013 11:02
Josef Kufner | skóre: 70
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.Tohle větou jsi měl celý článek uvést
Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?
Nejspíš ne.
Konkrétně, pokud máte na mysli podobnou definici
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = y + res ≡ x
tak ne. Problém je v tom, že pro x < y neexistuje přirozené číslo res a Auto hledá totální funkci (všude definovanou).
Kdybych zadefinoval relaci ≥ a funkci binop₂ definoval pouze pro x ≥ y, tak by to stejně nenašel – je to už příliš složité. Nezkoušel jsem to, ale myslím, že by se muselo nadefinovat ∸, pak dokázat lemma, že z x ≥ y a x ∸ y ≡ res plyne y + res ≡ x, a pak by to našel (ale to už není příliš zajímavé, protože je to vlastně celé hotové).
Tiskni
Sdílej:
